set R = the Order of {{}};
take L = RelStr(# {{}}, the Order of {{}} #); :: thesis: ( L is reflexive & L is transitive & L is antisymmetric & L is strict & L is total & L is 1 -element )
A1: field the Order of {{}} = the carrier of L by ORDERS_1:12;
hence the InternalRel of L is_reflexive_in the carrier of L by RELAT_2:def 9; :: according to ORDERS_2:def 2 :: thesis: ( L is transitive & L is antisymmetric & L is strict & L is total & L is 1 -element )
thus the InternalRel of L is_transitive_in the carrier of L by A1, RELAT_2:def 16; :: according to ORDERS_2:def 3 :: thesis: ( L is antisymmetric & L is strict & L is total & L is 1 -element )
thus the InternalRel of L is_antisymmetric_in the carrier of L by A1, RELAT_2:def 12; :: according to ORDERS_2:def 4 :: thesis: ( L is strict & L is total & L is 1 -element )
thus L is strict ; :: thesis: ( L is total & L is 1 -element )
thus the InternalRel of L is total ; :: according to ORDERS_2:def 1 :: thesis: L is 1 -element
thus the carrier of L is 1 -element ; :: according to STRUCT_0:def 19 :: thesis: verum