A1: now :: thesis: for R being set st R in LinOrders A holds

R is connected Order of A

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;

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

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;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

then
A c= dom R9
by TARSKI:def 3;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;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

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

then
A c= rng R9
by TARSKI:def 3;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;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

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

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

R in LinOrders A

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

[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;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 )

for a, b, c being Element of A st [a,b] in R & [b,c] in R 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;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

[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

( 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 )

hence
it0 = LinOrders A
by TARSKI:2; :: thesis: verum( 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;( 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