use(verband).

% We don't get this one at present.

%goal 
%A >= B, lub(A,C) = lub(B,C), glb(A,C) = glb(B,C) -> A = B.

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