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
reconsider R9 = R as Relation of A by A2, Def1;

A3: now

let a be set ; :: thesis: ( a in A implies a in dom R9 )
assume A4: a in A ; :: thesis: a in dom R9
A5: [a,a] in R by A2, A4, Def1;
thus a in dom R9 by A5, RELAT_1:def 4; :: thesis: verum

end;

A6: A c= dom R9 by A3, TARSKI:def 3;
A7: dom R9 = A by A6, XBOOLE_0:def 10;

A8: now

let a be set ; :: thesis: ( a in A implies a in rng R9 )
assume A9: a in A ; :: thesis: a in rng R9
A10: [a,a] in R by A2, A9, Def1;
thus a in rng R9 by A10, RELAT_1:def 5; :: thesis: verum

end;

A11: A c= rng R9 by A8, TARSKI:def 3;
A12: field R9 = A \/ A by A7, A11, XBOOLE_0:def 10;
A13: 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;
A14: R9 is_connected_in A by A13, RELAT_2:def 6;
A15: for a being set st a in A holds
[a,a] in R by A2, Def1;
A16: R9 is_reflexive_in A by A15, RELAT_2:def 1;
A17: 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;
A18: R9 is_antisymmetric_in A by A17, RELAT_2:def 4;
A19: 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;
A20: R9 is_transitive_in A by A19, RELAT_2:def 8;
thus R is connected Order of A by A7, A12, A14, A16, A18, A20, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16; :: thesis: verum

end;

A21: now

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

A23: now

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

end;

A29: for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R by A22, ORDERS_1:14;
A30: R in LinPreorders A by A22, A23, A29, Def1;
A31: for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b by A22, ORDERS_1:13;
thus R in LinOrders A by A30, A31, 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, A21; :: thesis: ( ( for R being set holds
( R in it0 iff R is connected Order of A ) ) implies it0 = LinOrders A )
assume A32: for R being set holds
( R in it0 iff R is connected Order of A ) ; :: thesis: it0 = LinOrders A

A33: now

let R be set ; :: thesis: ( R in it0 iff R in LinOrders A )
A34: ( R in it0 iff R is connected Order of A ) by A32;
thus ( R in it0 iff R in LinOrders A ) by A1, A21, A34; :: thesis: verum

end;

thus it0 = LinOrders A by A33, TARSKI:2; :: thesis: verum