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 completely-distributive ; :: thesis: verum