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