A=<B, B=<C -> A=<C.
A=<A.

A=<B -> f(A)=<f(B).

elem(A,S),S=<S1 -> elem(A,S1).
elem(A,o) -> f(A)=<A.
f(A)=<A -> elem(A,o).

elem(A,o) -> glb(o)=<A.

goal
f(glb(o))=glb(o) -> [].