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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
then R9 is_transitive_in A by RELAT_2:def 8;
hence R is connected Order of A by ; :: 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:
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 ;
( a = b or a <> b ) ;
hence ( [a,b] in R or [b,a] in R ) by ; :: 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 ;
then A13: R in LinPreorders A by ;
for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b by ;
hence R in LinOrders A by ; :: thesis: verum
end;
let it0 be Subset of (); :: 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