let R be Relation; :: thesis: ( R is well-ordering implies for a being set 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 set st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic
then A2: R is antisymmetric by Def4;
let a be set ; :: thesis: ( a in field R implies not R,R |_2 (R -Seg a) are_isomorphic )
assume A3: 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 A4: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is_isomorphism_of R,R |_2 (R -Seg a) by A1, Def9;
then A5: dom (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field R by Def7;
A6: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is one-to-one by A4, Def7;

A7: now

let b, c be set ; :: 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
A8: [b,c] in R and
A9: 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 A4, A8, Def7;
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 A8, 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 A5, A6, A9, FUNCT_1:def 4; :: thesis: verum

end;

A10: rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field (R |_2 (R -Seg a)) by A4, Def7;
field (R |_2 (R -Seg a)) = R -Seg a by A1, Th40;
then (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a in R -Seg a by A3, A5, A10, FUNCT_1:def 3;
then A11: ( [((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 A10, Th20;
then [a,((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a)] in R by A1, A3, A5, A7, Th43;
hence contradiction by A2, A11, Lm3; :: thesis: verum