consider x being set , R being Order of {x};
RelStr(# {x},R #) is non empty trivial RelStr ;
hence ex b₁ being LATTICE st
( b₁ is continuous & b₁ is complete & b₁ is strict ) ; :: thesis: verum