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