let R be Relation; ( 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
; for a being object st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic
let a be object ; ( a in field R implies not R,R |_2 (R -Seg a) are_isomorphic )
assume A2:
a in field R
; 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
; 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 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 )let b,
c be
object ;
( [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
;
( [((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;
(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;
verum end;
A9:
rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field (R |_2 (R -Seg a))
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; verum