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 ; :: 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 ; :: 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 ;
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 ;
then A9: ( x = {} & y = {} ) by ZFMISC_1:3;
[x,x] in the Order of by ;
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