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