set x = the set ;
set R = the Order of { the set };
RelStr(# { the set }, the Order of { the set } #) is 1 -element RelStr ;
hence ex b₁ being LATTICE st
( b₁ is continuous & b₁ is complete & b₁ is strict ) ; :: thesis: verum