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