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