use(mod_verband).

goal a >= b.
goal lub(a,c) = lub(b,c).
goal glb(a,c) = glb(b,c).
goal a = b -> [].