A1: now :: thesis: for R being set st R in LinOrders A holds
R is connected Order of A

let R be set ; :: thesis: ( R in LinOrders A implies R is connected Order of A )
assume A2: R in LinOrders A ; :: thesis: R is connected Order of A
then reconsider R9 = R as Relation of A by Def1;

now :: thesis: for a being object st a in A holds
a in dom R9

let a be object ; :: thesis: ( a in A implies a in dom R9 )
assume a in A ; :: thesis: a in dom R9
then [a,a] in R by A2, Def1;
hence a in dom R9 by XTUPLE_0:def 12; :: thesis: verum

end;

then A c= dom R9 by TARSKI:def 3;
then A3: dom R9 = A by XBOOLE_0:def 10;

now :: thesis: for a being object st a in A holds
a in rng R9

let a be object ; :: thesis: ( a in A implies a in rng R9 )
assume a in A ; :: thesis: a in rng R9
then [a,a] in R by A2, Def1;
hence a in rng R9 by XTUPLE_0:def 13; :: thesis: verum

end;

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; :: thesis: verum

end;

A8: now :: thesis: for R being set st R is connected Order of A holds
R in LinOrders A

let R be set ; :: thesis: ( R is connected Order of A implies R in LinOrders A )
assume A9: R is connected Order of A ; :: thesis: R in LinOrders A
then reconsider R9 = R as connected Order of A ;

A10: now :: thesis: for a, b being Element of A holds
( [a,b] in R or [b,a] in R )

let a, b be Element of A; :: thesis: ( [a,b] in R or [b,a] in R )
dom R9 = A by PARTFUN1:def 2;
then A c= (dom R9) \/ (rng R9) by XBOOLE_1:7;
then A11: field R9 = A by XBOOLE_0:def 10;
A12: ( R9 is_connected_in field R9 & R9 is_reflexive_in field R9 ) by RELAT_2:def 9, RELAT_2:def 14;
( a = b or a <> b ) ;
hence ( [a,b] in R or [b,a] in R ) by A11, A12, RELAT_2:def 1, RELAT_2:def 6; :: thesis: verum

end;

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; :: thesis: verum

end;

let it0 be Subset of (LinPreorders A); :: thesis: ( 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; :: thesis: ( ( 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 ) ; :: thesis: it0 = LinOrders A

now :: thesis: for R being object holds
( R in it0 iff R in LinOrders A )

let R be object ; :: thesis: ( R in it0 iff R in LinOrders A )
( R in it0 iff R is connected Order of A ) by A14;
hence ( R in it0 iff R in LinOrders A ) by A1, A8; :: thesis: verum

end;

hence it0 = LinOrders A by TARSKI:2; :: thesis: verum