A1: now

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 R' = R as Relation of A by Def1;

now

let a be set ; :: thesis: ( a in A implies a in dom R' )
assume a in A ; :: thesis: a in dom R'
then [a,a] in R by A2, Def1;
hence a in dom R' by RELAT_1:def 4; :: thesis: verum

end;

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

now

let a be set ; :: thesis: ( a in A implies a in rng R' )
assume a in A ; :: thesis: a in rng R'
then [a,a] in R by A2, Def1;
hence a in rng R' by RELAT_1:def 5; :: thesis: verum

end;

then A c= rng R' by TARSKI:def 3;
then A4: field R' = A \/ A by A3, XBOOLE_0:def 10;
for a, b being set st a in A & b in A & a <> b & not [a,b] in R holds
[b,a] in R by A2, Def1;
then A5: R' is_connected_in A by RELAT_2:def 6;
for a being set st a in A holds
[a,a] in R by A2, Def1;
then A6: R' is_reflexive_in A by RELAT_2:def 1;
for a, b being set st a in A & b in A & [a,b] in R & [b,a] in R holds
a = b by A2, Def2;
then A7: R' is_antisymmetric_in A by RELAT_2:def 4;
for a, b, c being set 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 R' is_transitive_in A by RELAT_2:def 8;
hence R is connected Order of A by A3, A4, A5, A6, A7, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16; :: thesis: verum

end;

A8: now

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 R' = R as connected Order of A ;

A10: now

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

end;

( R is Relation 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:14;
then ( R in LinPreorders A & ( for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) by A9, A10, Def1, ORDERS_1:13;
hence R in LinOrders A by 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 A11: for R being set holds
( R in it0 iff R is connected Order of A ) ; :: thesis: it0 = LinOrders A

now

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

end;

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