set x = the set ;
set O = the Order of { the set };
RelStr(# { the set }, the Order of { the set } #) is non empty trivial RelStr ;
hence ex b₁ being non empty Chain st b₁ is complete ; :: thesis: verum