let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_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); Upper_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:
N-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:39;
A2:
(Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n)))
by JORDAN9:32;
then
(E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by SPRECT_2:72;
then
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:71, XXREAL_0:2;
then A3:
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:73, XXREAL_0:2;
then A4:
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:74, XXREAL_0:2;
((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) /. 1 = E-max (L~ (Cage (C,n)))
by FINSEQ_5:53;
then A5:
E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by FINSEQ_6:42;
A6:
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
then ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) =
(Cage (C,n)) /. (len (Cage (C,n)))
by FINSEQ_5:54
.=
(Cage (C,n)) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:32
;
then A7:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by FINSEQ_6:168;
{(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by A7, A5, TARSKI:def 2;
then A8:
card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))))
by CARD_1:11;
A9:
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
then A10:
(Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) <> {}
by FINSEQ_5:47;
len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, FINSEQ_5:42;
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 A9, FINSEQ_5:45;
then A11:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A10, FINSEQ_6:168;
((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. 1 =
(Cage (C,n)) /. 1
by A9, FINSEQ_5:44
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:32
;
then A12:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A10, FINSEQ_6:42;
{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A12, A11, TARSKI:def 2;
then A13:
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:11;
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:61;
then A14:
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:62;
A15:
(N-min (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:52;
(N-max (L~ (Cage (C,n)))) `1 <= (NE-corner (L~ (Cage (C,n)))) `1
by PSCOMP_1:38;
then A16:
(N-max (L~ (Cage (C,n)))) `1 <= E-bound (L~ (Cage (C,n)))
by EUCLID:52;
(N-min (L~ (Cage (C,n)))) `1 < (N-max (L~ (Cage (C,n)))) `1
by SPRECT_2:51;
then A17:
N-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n)))
by A16, EUCLID:52;
then A18:
card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} = 2
by CARD_2:57;
A19:
(S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:74;
then A20:
E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A9, A6, A3, FINSEQ_5:46, XXREAL_0:2;
A21:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by A9, A6, A19, A3, FINSEQ_6:62, XXREAL_0:2;
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:13;
then
(W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2
by A15, PSCOMP_1:24;
then A22:
N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n)))
by SPRECT_2:57;
then
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2
by CARD_2:57;
then
Segm 2 c= Segm (len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))))
by A13, A14;
then
len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) >= 2
by NAT_1:39;
then A23:
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;
A24:
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:53;
then A25:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by FINSEQ_6:42;
((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 A9, FINSEQ_5:54
.=
(Cage (C,n)) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:32
;
then A26:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by FINSEQ_6:168;
{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by A26, A25, TARSKI:def 2;
then A27:
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:11;
A28:
(N-min (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:52;
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:13;
then
(W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2
by A28, PSCOMP_1:24;
then
N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n)))
by SPRECT_2:57;
then A29:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2
by CARD_2:57;
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:61;
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:62;
then
Segm 2
c= Segm (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by A29, A27;
then
len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2
by NAT_1:39;
then A30:
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 A20, A23, A30, 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 JORDAN1G:17;
then
E-max (L~ (Cage (C,n))) = W-min (L~ (Cage (C,n)))
by A17, TARSKI:def 2;
hence
contradiction
by TOPREAL5:19;
verum
end;
A31:
(N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:70;
A32:
(N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:68;
then A33:
(N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A2, SPRECT_2:70, XXREAL_0:2;
then A34:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))
by A1, A9, A4, FINSEQ_5:46, XXREAL_0:2;
A35:
(E-max (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) <> 1
proof
assume A36:
(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 A1, A9, A33, A4, SPRECT_5:3, XXREAL_0:2
.=
1
by A2, FINSEQ_6:43
;
hence
contradiction
by A32, A31, A20, A34, A36, FINSEQ_5:9;
verum
end;
then
E-max (L~ (Cage (C,n))) in rng (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)
by A20, FINSEQ_6:78;
then A37:
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 A24, XBOOLE_0:def 5;
card (rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))))
by CARD_2:61;
then
card (rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by CARD_1:62;
then
Segm 2 c= Segm (len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))))
by A18, A8;
then
len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) >= 2
by NAT_1:39;
then A38:
rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))
by SPPOL_2:18;
not W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
proof
assume A39:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
;
contradiction
((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) =
((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))
by A6, FINSEQ_5:42
.=
E-max (L~ (Cage (C,n)))
by A6, FINSEQ_5:45
;
then A40:
E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
by A39, RELAT_1:38, FINSEQ_6:168;
((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /. 1 =
(Cage (C,n)) /. 1
by A6, FINSEQ_5:44
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:32
;
then A41:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
by A39, FINSEQ_6:42, RELAT_1:38;
{(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
by A41, A40, TARSKI:def 2;
then A42:
card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))))
by CARD_1:11;
card (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))))
by CARD_2:61;
then
card (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
by CARD_1:62;
then
Segm 2
c= Segm (len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))))
by A18, A42;
then
len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) >= 2
by NAT_1:39;
then
rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))
by SPPOL_2:18;
then
W-min (L~ (Cage (C,n))) in (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))))
by A21, A38, A39, XBOOLE_0:def 4;
then
W-min (L~ (Cage (C,n))) in {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by Th3;
then
W-min (L~ (Cage (C,n))) = E-max (L~ (Cage (C,n)))
by A22, TARSKI:def 2;
hence
contradiction
by TOPREAL5:19;
verum
end;
then A43:
W-min (L~ (Cage (C,n))) in (rng (Cage (C,n))) \ (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))))
by A9, XBOOLE_0:def 5;
(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 A9, FINSEQ_6:def 2
.=
((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 A37, FINSEQ_6:67
.=
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) ^ ((((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) -: (E-max (L~ (Cage (C,n))))) /^ 1)
by A20, A35, FINSEQ_6:60
.=
(((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) :- (W-min (L~ (Cage (C,n))))) ^ ((((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) -: (E-max (L~ (Cage (C,n))))) /^ 1)
by A43, FINSEQ_6:71, SPRECT_2:46
.=
(((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) :- (W-min (L~ (Cage (C,n))))) ^ (((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /^ 1)
by A9, A20, FINSEQ_6:75
.=
(((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 A21, FINSEQ_6:64
.=
(Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n))))
by A6, FINSEQ_6:def 2
;
hence
Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n))))
by JORDAN1E:def 1; verum