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 {{}}

for x, y being object st x in {{}} & y in {{}} & not [x,y] in the Order of {{}} holds

[y,x] in the Order of {{}}

thus L is strict ; :: thesis: L is total

thus the InternalRel of L is total ; :: according to ORDERS_2:def 1 :: thesis: verum

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

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 )
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;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

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

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 )
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;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

thus L is strict ; :: thesis: L is total

thus the InternalRel of L is total ; :: according to ORDERS_2:def 1 :: thesis: verum