set R = the Order of {{}};
take L = RelStr(# {{}}, the Order of {{}} #); :: thesis: ( not L is empty & L is reflexive & L is transitive & L is antisymmetric & L is connected & L is strongly_connected & L is strict & L is total )
thus not L is empty ; :: thesis: ( L is reflexive & L is transitive & L is antisymmetric & L is connected & L is strongly_connected & L is strict & L is total )
A1: field the Order of {{}} = the carrier of L by ORDERS_1:12;
hence A2: 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 connected & L is strongly_connected & 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 3 :: thesis: ( L is antisymmetric & L is connected & L is strongly_connected & 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 4 :: thesis: ( L is connected & L is strongly_connected & L is strict & L is total )
for x, y being object st x in {{}} & y in {{}} & x <> y & not [x,y] in the Order of {{}} holds
[y,x] in the Order of {{}}

proof

let x, y be object ; :: thesis: ( x in {{}} & y in {{}} & x <> y & not [x,y] in the Order of {{}} implies [y,x] in the Order of {{}} )
assume that
A3: x in {{}} and
A4: y in {{}} and
A5: x <> y ; :: thesis: ( [x,y] in the Order of {{}} or [y,x] in the Order of {{}} )
( {x} c= {{}} & {y} c= {{}} ) by A3, A4, ZFMISC_1:31;
then A6: ( x = {} & y = {} ) by ZFMISC_1:3;
assume ( not [x,y] in the Order of {{}} & not [y,x] in the Order of {{}} ) ; :: thesis: contradiction
thus contradiction by A5, A6; :: thesis: verum

end;

hence the InternalRel of L is_connected_in the carrier of L by RELAT_2:def 6; :: according to ORDERS_5:def 1 :: thesis: ( L is strongly_connected & L is strict & L is total )
for x, y being object st x in {{}} & y in {{}} & not [x,y] in the Order of {{}} holds
[y,x] in the Order of {{}}

proof

let x, y be object ; :: thesis: ( x in {{}} & y in {{}} & not [x,y] in the Order of {{}} implies [y,x] in the Order of {{}} )
assume that
A7: x in {{}} and
A8: y in {{}} ; :: thesis: ( [x,y] in the Order of {{}} or [y,x] in the Order of {{}} )
( {x} c= {{}} & {y} c= {{}} ) by A7, A8, ZFMISC_1:31;
then A9: ( x = {} & y = {} ) by ZFMISC_1:3;
[x,x] in the Order of {{}} by A2, A7, RELAT_2:def 1;
hence ( [x,y] in the Order of {{}} or [y,x] in the Order of {{}} ) by A9; :: thesis: verum

end;

hence the InternalRel of L is_strongly_connected_in the carrier of L by RELAT_2:def 7; :: according to ORDERS_5:def 2 :: 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 1 :: thesis: verum