consider O being Order of {{} };
take RelStr(# {{} },O #) ; :: thesis: ( RelStr(# {{} },O #) is strict & RelStr(# {{} },O #) is trivial & not RelStr(# {{} },O #) is empty & RelStr(# {{} },O #) is reflexive )
thus ( RelStr(# {{} },O #) is strict & RelStr(# {{} },O #) is trivial & not RelStr(# {{} },O #) is empty & RelStr(# {{} },O #) is reflexive ) ; :: thesis: verum