set x = the set ;
set R = the Order of { the set };
RelStr(# { the set }, the Order of { the set } #) is non empty trivial RelStr ;
hence ex b₁ being LATTICE st b₁ is completely-distributive ; :: thesis: verum