set R = the Order of {{}};
take L = RelStr(# {{}}, the Order of {{}} #); ( 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
; ( 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; ORDERS_2:def 2 ( 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; ORDERS_2:def 3 ( 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; ORDERS_2:def 4 ( 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 ;
( 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
;
( [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
{{}} )
;
contradiction
thus
contradiction
by A5, A6;
verum
end;
hence
the InternalRel of L is_connected_in the carrier of L
by RELAT_2:def 6; ORDERS_5:def 1 ( 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 ;
( 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 {{}}
;
( [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;
verum
end;
hence
the InternalRel of L is_strongly_connected_in the carrier of L
by RELAT_2:def 7; ORDERS_5:def 2 ( L is strict & L is total )
thus
L is strict
; L is total
thus
the InternalRel of L is total
; ORDERS_2:def 1 verum