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
assume A4: R,R |_2 (R -Seg a) are_isomorphic ; :: thesis: contradiction
set S = R |_2 (R -Seg a);
set F = canonical_isomorphism_of R,(R |_2 (R -Seg a));
A5: canonical_isomorphism_of R,(R |_2 (R -Seg a)) is_isomorphism_of R,R |_2 (R -Seg a) by A1, A4, Def9;
then A6: ( dom (canonical_isomorphism_of R,(R |_2 (R -Seg a))) = field R & rng (canonical_isomorphism_of R,(R |_2 (R -Seg a))) = field (R |_2 (R -Seg a)) & canonical_isomorphism_of R,(R |_2 (R -Seg a)) is one-to-one & ( for c, b being set holds
( [c,b] in R iff ( c in field R & b in field R & [((canonical_isomorphism_of R,(R |_2 (R -Seg a))) . c),((canonical_isomorphism_of R,(R |_2 (R -Seg a))) . b)] in R |_2 (R -Seg a) ) ) ) ) by Def7;
then A7: rng (canonical_isomorphism_of R,(R |_2 (R -Seg a))) c= field R by Th20;

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 A8: ( [b,c] in R & 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 )
then [((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 A5, 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:30;
hence (canonical_isomorphism_of R,(R |_2 (R -Seg a))) . b <> (canonical_isomorphism_of R,(R |_2 (R -Seg a))) . c by A6, A8, FUNCT_1:def 8; :: thesis: verum

end;

then A9: [a,((canonical_isomorphism_of R,(R |_2 (R -Seg a))) . a)] in R by A1, A3, A6, A7, Th43;
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, A6, FUNCT_1:def 5;
then ( [((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 Def1;
hence contradiction by A2, A9, Lm3; :: thesis: verum