let n be Element of 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:43;
A2:
(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 A2, SPRECT_2:75, 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:77, 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:78, XXREAL_0:2;
((Cage C,n) :- (E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Cage C,n))
by FINSEQ_5:56;
then A5:
E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by FINSEQ_6:46;
A6:
E-max (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:50;
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:57
.=
(Cage C,n) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A7:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by REVROT_1:3;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
proof
let x be
set ;
TARSKI:def 3 ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) )
assume
x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))}
;
x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
hence
x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by A7, A5, TARSKI:def 2;
verum
end;
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:27;
A9:
W-min (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:47;
then A10:
(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 A9, 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 A9, FINSEQ_5:48;
then A11:
W-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))
by A10, REVROT_1:3;
((Cage C,n) -: (W-min (L~ (Cage C,n)))) /. 1 =
(Cage C,n) /. 1
by A9, FINSEQ_5:47
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A12:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))
by A10, 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 A12, A11, TARSKI:def 2;
verum
end;
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: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 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:104;
A15:
(N-min (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n))
by EUCLID:56;
(N-max (L~ (Cage C,n))) `1 <= (NE-corner (L~ (Cage C,n))) `1
by PSCOMP_1:97;
then A16:
(N-max (L~ (Cage C,n))) `1 <= E-bound (L~ (Cage C,n))
by EUCLID:56;
(N-min (L~ (Cage C,n))) `1 < (N-max (L~ (Cage C,n))) `1
by SPRECT_2:55;
then A17:
N-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n))
by A16, EUCLID:56;
then A18:
card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 2
by CARD_2:76;
A19:
(S-min (L~ (Cage C,n))) .. (Cage C,n) <= (W-min (L~ (Cage C,n))) .. (Cage C,n)
by A2, SPRECT_2:78;
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:49, 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:67, XXREAL_0:2;
W-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:15;
then
(W-max (L~ (Cage C,n))) `2 <= (N-min (L~ (Cage C,n))) `2
by A15, PSCOMP_1:71;
then A22:
N-min (L~ (Cage C,n)) <> W-min (L~ (Cage C,n))
by SPRECT_2:61;
then
card {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} = 2
by CARD_2:76;
then
2 c= len ((Cage C,n) -: (W-min (L~ (Cage C,n))))
by A13, A14, XBOOLE_1:1;
then
len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) >= 2
by NAT_1:40;
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:56;
then A25:
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 A9, FINSEQ_5:57
.=
(Cage C,n) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A26:
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 A26, A25, TARSKI:def 2;
verum
end;
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:27;
A28:
(N-min (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n))
by EUCLID:56;
W-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:15;
then
(W-max (L~ (Cage C,n))) `2 <= (N-min (L~ (Cage C,n))) `2
by A28, PSCOMP_1:71;
then
N-min (L~ (Cage C,n)) <> W-min (L~ (Cage C,n))
by SPRECT_2:61;
then A29:
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 A29, A27, XBOOLE_1:1;
then
len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) >= 2
by NAT_1:40;
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:25;
then
E-max (L~ (Cage C,n)) = W-min (L~ (Cage C,n))
by A17, TARSKI:def 2;
hence
contradiction
by TOPREAL5:25;
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:74;
A32:
(N-min (L~ (Cage C,n))) .. (Cage C,n) < (N-max (L~ (Cage C,n))) .. (Cage C,n)
by A2, SPRECT_2:72;
then A33:
(N-min (L~ (Cage C,n))) .. (Cage C,n) < (E-max (L~ (Cage C,n))) .. (Cage C,n)
by A2, SPRECT_2:74, 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:49, 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:47
;
hence
contradiction
by A32, A31, A20, A34, A36, 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 A20, FINSEQ_6:83;
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:80;
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:104;
then
2 c= len ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by A18, A8, XBOOLE_1:1;
then
len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) >= 2
by NAT_1:40;
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:45
.=
E-max (L~ (Cage C,n))
by A6, FINSEQ_5:48
;
then A40:
E-max (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A39, RELAT_1:60, REVROT_1:3;
((Cage C,n) -: (E-max (L~ (Cage C,n)))) /. 1 =
(Cage C,n) /. 1
by A6, FINSEQ_5:47
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A41:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A39, FINSEQ_6:46, RELAT_1:60;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
proof
let x be
set ;
TARSKI:def 3 ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) )
assume
x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))}
;
x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
hence
x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A41, A40, TARSKI:def 2;
verum
end;
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:27;
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:80;
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:104;
then
2
c= len ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A18, A42, XBOOLE_1:1;
then
len ((Cage C,n) -: (E-max (L~ (Cage C,n)))) >= 2
by NAT_1:40;
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:25;
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:72
.=
((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:65
.=
(((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:76, SPRECT_2:50
.=
(((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:80
.=
(((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:69
.=
(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