set O = the Order of {{}};
take RelStr(# {{}}, the Order of {{}} #) ; :: thesis: ( RelStr(# {{}}, the Order of {{}} #) is strict & RelStr(# {{}}, the Order of {{}} #) is 1 -element & RelStr(# {{}}, the Order of {{}} #) is reflexive )
thus ( RelStr(# {{}}, the Order of {{}} #) is strict & RelStr(# {{}}, the Order of {{}} #) is 1 -element & RelStr(# {{}}, the Order of {{}} #) is reflexive ) ; :: thesis: verum