A1:
now for R being set st R in LinOrders A holds
R is connected Order of Alet R be
set ;
( R in LinOrders A implies R is connected Order of A )assume A2:
R in LinOrders A
;
R is connected Order of Athen reconsider R9 =
R as
Relation of
A by Def1;
then
A c= dom R9
by TARSKI:def 3;
then A3:
dom R9 = A
by XBOOLE_0:def 10;
then
A c= rng R9
by TARSKI:def 3;
then A4:
field R9 = A \/ A
by A3, XBOOLE_0:def 10;
for
a,
b being
object st
a in A &
b in A &
a <> b & not
[a,b] in R holds
[b,a] in R
by A2, Def1;
then A5:
R9 is_connected_in A
by RELAT_2:def 6;
for
a being
object st
a in A holds
[a,a] in R
by A2, Def1;
then A6:
R9 is_reflexive_in A
by RELAT_2:def 1;
for
a,
b being
object st
a in A &
b in A &
[a,b] in R &
[b,a] in R holds
a = b
by A2, Def2;
then A7:
R9 is_antisymmetric_in A
by RELAT_2:def 4;
for
a,
b,
c being
object st
a in A &
b in A &
c in A &
[a,b] in R &
[b,c] in R holds
[a,c] in R
by A2, Def1;
then
R9 is_transitive_in A
by RELAT_2:def 8;
hence
R is
connected Order of
A
by A3, A4, A5, A6, A7, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16;
verum end;
A8:
now for R being set st R is connected Order of A holds
R in LinOrders Alet R be
set ;
( R is connected Order of A implies R in LinOrders A )assume A9:
R is
connected Order of
A
;
R in LinOrders Athen reconsider R9 =
R as
connected Order of
A ;
for
a,
b,
c being
Element of
A st
[a,b] in R &
[b,c] in R holds
[a,c] in R
by A9, ORDERS_1:5;
then A13:
R in LinPreorders A
by A9, A10, Def1;
for
a,
b being
Element of
A st
[a,b] in R &
[b,a] in R holds
a = b
by A9, ORDERS_1:4;
hence
R in LinOrders A
by A13, Def2;
verum end;
let it0 be Subset of (LinPreorders A); ( it0 = LinOrders A iff for R being set holds
( R in it0 iff R is connected Order of A ) )
thus
( it0 = LinOrders A implies for R being set holds
( R in it0 iff R is connected Order of A ) )
by A1, A8; ( ( for R being set holds
( R in it0 iff R is connected Order of A ) ) implies it0 = LinOrders A )
assume A14:
for R being set holds
( R in it0 iff R is connected Order of A )
; it0 = LinOrders A
hence
it0 = LinOrders A
by TARSKI:2; verum