let R be Relation; :: thesis: ( R is well-ordering implies for a being object st a in field R holds

not R,R |_2 (R -Seg a) are_isomorphic )

assume A1: R is well-ordering ; :: thesis: for a being object st a in field R holds

not R,R |_2 (R -Seg a) are_isomorphic

let a be object ; :: thesis: ( a in field R implies not R,R |_2 (R -Seg a) are_isomorphic )

assume A2: a in field R ; :: thesis: not R,R |_2 (R -Seg a) are_isomorphic

set S = R |_2 (R -Seg a);

set F = canonical_isomorphism_of (R,(R |_2 (R -Seg a)));

assume R,R |_2 (R -Seg a) are_isomorphic ; :: thesis: contradiction

then A3: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is_isomorphism_of R,R |_2 (R -Seg a) by A1, Def9;

then A4: dom (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field R ;

A5: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is one-to-one by A3;

field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;

then (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a in R -Seg a by A2, A4, A9, FUNCT_1:def 3;

then A10: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a),a] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a <> a ) by Th1;

rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) c= field R by A9, Th13;

then [a,((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a)] in R by A1, A2, A4, A6, Th35;

hence contradiction by A1, A10, Lm3; :: thesis: verum

not R,R |_2 (R -Seg a) are_isomorphic )

assume A1: R is well-ordering ; :: thesis: for a being object st a in field R holds

not R,R |_2 (R -Seg a) are_isomorphic

let a be object ; :: thesis: ( a in field R implies not R,R |_2 (R -Seg a) are_isomorphic )

assume A2: a in field R ; :: thesis: not R,R |_2 (R -Seg a) are_isomorphic

set S = R |_2 (R -Seg a);

set F = canonical_isomorphism_of (R,(R |_2 (R -Seg a)));

assume R,R |_2 (R -Seg a) are_isomorphic ; :: thesis: contradiction

then A3: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is_isomorphism_of R,R |_2 (R -Seg a) by A1, Def9;

then A4: dom (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field R ;

A5: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is one-to-one by A3;

A6: now :: thesis: for b, c being object st [b,c] in R & b <> c holds

( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )

A9:
rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field (R |_2 (R -Seg a))
by A3;( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )

let b, c be object ; :: thesis: ( [b,c] in R & b <> c implies ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c ) )

assume that

A7: [b,c] in R and

A8: b <> c ; :: thesis: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )

[((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R |_2 (R -Seg a) by A3, A7;

hence [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R by XBOOLE_0:def 4; :: thesis: (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c

( b in field R & c in field R ) by A7, RELAT_1:15;

hence (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c by A4, A5, A8; :: thesis: verum

end;assume that

A7: [b,c] in R and

A8: b <> c ; :: thesis: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )

[((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R |_2 (R -Seg a) by A3, A7;

hence [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R by XBOOLE_0:def 4; :: thesis: (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c

( b in field R & c in field R ) by A7, RELAT_1:15;

hence (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c by A4, A5, A8; :: thesis: verum

field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;

then (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a in R -Seg a by A2, A4, A9, FUNCT_1:def 3;

then A10: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a),a] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a <> a ) by Th1;

rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) c= field R by A9, Th13;

then [a,((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a)] in R by A1, A2, A4, A6, Th35;

hence contradiction by A1, A10, Lm3; :: thesis: verum