consider x1 being set , R being Order of {x1};
reconsider RS = RelStr(# {x1},R #) as non empty trivial 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