set x1 = the set ;
set R = the Order of { the set };
reconsider RS = RelStr(# { the set }, the Order of { the set } #) as 1 -element reflexive RelStr ;
take RS ; :: thesis: ( RS is strict & RS is continuous & RS is distributive & RS is lower-bounded )
thus ( RS is strict & RS is continuous & RS is distributive & RS is lower-bounded ) ; :: thesis: verum