let n be Element of NAT ; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
set Nmi = N-min (L~ (Cage (C,n)));
set Nma = N-max (L~ (Cage (C,n)));
set Wmi = W-min (L~ (Cage (C,n)));
set Wma = W-max (L~ (Cage (C,n)));
set Ema = E-max (L~ (Cage (C,n)));
set Emi = E-min (L~ (Cage (C,n)));
set Sma = S-max (L~ (Cage (C,n)));
set Smi = S-min (L~ (Cage (C,n)));
set RotWmi = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
set RotEma = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));
A1:
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:50;
( W-max (L~ (Cage (C,n))) in L~ (Cage (C,n)) & (N-min (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) )
by EUCLID:56, SPRECT_1:15;
then
(W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:71;
then
N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n)))
by SPRECT_2:61;
then A2:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2
by CARD_2:76;
A3:
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:47;
then A4:
(Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) <> {}
by FINSEQ_5:50;
len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A3, FINSEQ_5:45;
then
((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) = W-min (L~ (Cage (C,n)))
by A3, FINSEQ_5:48;
then A5:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A4, REVROT_1:3;
((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. 1 =
(Cage (C,n)) /. 1
by A3, FINSEQ_5:47
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:34
;
then A6:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A4, FINSEQ_6:46;
{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
proof
let x be
set ;
TARSKI:def 3 ( not x in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} or x in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) )
assume
x in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
;
x in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
hence
x in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A6, A5, TARSKI:def 2;
verum
end;
then A7:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))))
by CARD_1:27;
card (rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))))
by CARD_2:80;
then
card (rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by CARD_1:104;
then
2 c= len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A2, A7, XBOOLE_1:1;
then
len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) >= 2
by NAT_1:40;
then A8:
rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by SPPOL_2:18;
A9:
(Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n)))
by JORDAN9:34;
then
(E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by SPRECT_2:76;
then
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:75, XXREAL_0:2;
then A10:
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:77, XXREAL_0:2;
then A11:
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:78, XXREAL_0:2;
A12:
(S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:78;
then A13:
E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A3, A1, A10, FINSEQ_5:49, XXREAL_0:2;
(N-max (L~ (Cage (C,n)))) `1 <= (NE-corner (L~ (Cage (C,n)))) `1
by PSCOMP_1:97;
then
( (N-min (L~ (Cage (C,n)))) `1 < (N-max (L~ (Cage (C,n)))) `1 & (N-max (L~ (Cage (C,n)))) `1 <= E-bound (L~ (Cage (C,n))) )
by EUCLID:56, SPRECT_2:55;
then A14:
N-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n)))
by EUCLID:56;
A15:
not E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
proof
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. 1
= W-min (L~ (Cage (C,n)))
by FINSEQ_5:56;
then A16:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by FINSEQ_6:46;
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) =
(Cage (C,n)) /. (len (Cage (C,n)))
by A3, FINSEQ_5:57
.=
(Cage (C,n)) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:34
;
then A17:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by REVROT_1:3;
{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
proof
let x be
set ;
TARSKI:def 3 ( not x in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} or x in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) )
assume
x in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
;
x in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
hence
x in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by A17, A16, TARSKI:def 2;
verum
end;
then A18:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by CARD_1:27;
(
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n)) &
(N-min (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) )
by EUCLID:56, SPRECT_1:15;
then
(W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:71;
then
N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n)))
by SPRECT_2:61;
then A19:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2
by CARD_2:76;
card (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by CARD_2:80;
then
card (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by CARD_1:104;
then
2
c= len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by A19, A18, XBOOLE_1:1;
then
len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2
by NAT_1:40;
then A20:
rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by SPPOL_2:18;
assume
E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
;
contradiction
then
E-max (L~ (Cage (C,n))) in (L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by A13, A8, A20, XBOOLE_0:def 4;
then
E-max (L~ (Cage (C,n))) in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
by Th25;
then
E-max (L~ (Cage (C,n))) = W-min (L~ (Cage (C,n)))
by A14, TARSKI:def 2;
hence
contradiction
by TOPREAL5:25;
verum
end;
A21:
(N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:74;
A22:
(N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:72;
then A23:
( N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & (N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) )
by A9, SPRECT_2:43, SPRECT_2:74, XXREAL_0:2;
then A24:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A3, A11, FINSEQ_5:49, XXREAL_0:2;
A25:
(E-max (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) <> 1
proof
assume A26:
(E-max (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = 1
;
contradiction
(N-min (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) =
(N-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A3, A23, A11, SPRECT_5:3, XXREAL_0:2
.=
1
by A9, FINSEQ_6:47
;
hence
contradiction
by A22, A21, A13, A24, A26, FINSEQ_5:10;
verum
end;
then
E-max (L~ (Cage (C,n))) in rng (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)
by A13, FINSEQ_6:83;
then A27:
E-max (L~ (Cage (C,n))) in (rng (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)) \ (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by A15, XBOOLE_0:def 5;
A28:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by A3, A1, A12, A10, FINSEQ_6:67, XXREAL_0:2;
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) =
(((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) ^ (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)) :- (E-max (L~ (Cage (C,n))))
by A3, FINSEQ_6:def 2
.=
(((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1) :- (E-max (L~ (Cage (C,n))))
by A27, FINSEQ_6:70
.=
((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) :- (E-max (L~ (Cage (C,n))))
by A13, A25, FINSEQ_6:89
.=
((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) -: (W-min (L~ (Cage (C,n))))
by A3, A1, A12, A10, Th24, XXREAL_0:2
.=
(((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) ^ (((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /^ 1)) -: (W-min (L~ (Cage (C,n))))
by A28, FINSEQ_6:71
.=
(Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
by A1, FINSEQ_6:def 2
;
hence
Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
by JORDAN1E:def 2; verum