let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ex k, t being Nat st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )
consider x being object such that
A1:
x in S-most C
by XBOOLE_0:def 1;
reconsider x = x as Point of (TOP-REAL 2) by A1;
A2:
x in C
by A1, XBOOLE_0:def 4;
set X = { q where q is Point of (TOP-REAL 2) : ( q `1 = x `1 & q `2 <= x `2 ) } ;
A3:
{ q where q is Point of (TOP-REAL 2) : ( q `1 = x `1 & q `2 <= x `2 ) } = south_halfline x
by TOPREAL1:34;
then reconsider X = { q where q is Point of (TOP-REAL 2) : ( q `1 = x `1 & q `2 <= x `2 ) } as connected Subset of (TOP-REAL 2) ;
assume A4:
for k, t being Nat st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) holds
(Cage (C,n)) /. k <> (Gauge (C,n)) * (t,1)
; contradiction
A5:
now x in UBD (L~ (Cage (C,n)))
south_halfline x meets L~ (Cage (C,n))
by A2, Th53;
then consider y being
object such that A6:
y in X
and A7:
y in L~ (Cage (C,n))
by A3, XBOOLE_0:3;
reconsider y =
y as
Point of
(TOP-REAL 2) by A6;
consider q being
Point of
(TOP-REAL 2) such that A8:
y = q
and A9:
q `1 = x `1
and A10:
q `2 <= x `2
by A6;
consider i being
Nat such that A11:
1
<= i
and A12:
i + 1
<= len (Cage (C,n))
and A13:
y in LSeg (
(Cage (C,n)),
i)
by A7, SPPOL_2:13;
A14:
q `2 < x `2
A15:
y in LSeg (
((Cage (C,n)) /. i),
((Cage (C,n)) /. (i + 1)))
by A11, A12, A13, TOPREAL1:def 3;
now x in UBD (L~ (Cage (C,n)))per cases
( ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 or ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 )
;
suppose
((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2
;
x in UBD (L~ (Cage (C,n)))then
((Cage (C,n)) /. i) `2 <= q `2
by A8, A15, TOPREAL1:4;
then A16:
((Cage (C,n)) /. i) `2 < x `2
by A14, XXREAL_0:2;
A17:
Cage (
C,
n)
is_sequence_on Gauge (
C,
n)
by JORDAN9:def 1;
A18:
i < len (Cage (C,n))
by A12, NAT_1:13;
then
i in Seg (len (Cage (C,n)))
by A11, FINSEQ_1:1;
then
i in dom (Cage (C,n))
by FINSEQ_1:def 3;
then consider i1,
i2 being
Nat such that A19:
[i1,i2] in Indices (Gauge (C,n))
and A20:
(Cage (C,n)) /. i = (Gauge (C,n)) * (
i1,
i2)
by A17, GOBOARD1:def 9;
A21:
1
<= i2
by A19, MATRIX_0:32;
A22:
i2 <= width (Gauge (C,n))
by A19, MATRIX_0:32;
A23:
( 1
<= i1 &
i1 <= len (Gauge (C,n)) )
by A19, MATRIX_0:32;
x `2 =
(S-min C) `2
by A1, PSCOMP_1:55
.=
S-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (i1,2)) `2
by A23, JORDAN8:13
;
then
i2 < 1
+ 1
by A16, A20, A22, A23, SPRECT_3:12;
then
i2 <= 1
by NAT_1:13;
then
(Cage (C,n)) /. i = (Gauge (C,n)) * (
i1,1)
by A20, A21, XXREAL_0:1;
hence
x in UBD (L~ (Cage (C,n)))
by A4, A11, A18, A23;
verum end; suppose
((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2
;
x in UBD (L~ (Cage (C,n)))then
q `2 >= ((Cage (C,n)) /. (i + 1)) `2
by A8, A15, TOPREAL1:4;
then A24:
((Cage (C,n)) /. (i + 1)) `2 < x `2
by A14, XXREAL_0:2;
A25:
Cage (
C,
n)
is_sequence_on Gauge (
C,
n)
by JORDAN9:def 1;
A26:
i + 1
>= 1
by NAT_1:11;
then
i + 1
in Seg (len (Cage (C,n)))
by A12, FINSEQ_1:1;
then
i + 1
in dom (Cage (C,n))
by FINSEQ_1:def 3;
then consider i1,
i2 being
Nat such that A27:
[i1,i2] in Indices (Gauge (C,n))
and A28:
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
i1,
i2)
by A25, GOBOARD1:def 9;
A29:
1
<= i2
by A27, MATRIX_0:32;
A30:
i2 <= width (Gauge (C,n))
by A27, MATRIX_0:32;
A31:
( 1
<= i1 &
i1 <= len (Gauge (C,n)) )
by A27, MATRIX_0:32;
x `2 =
(S-min C) `2
by A1, PSCOMP_1:55
.=
S-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (i1,2)) `2
by A31, JORDAN8:13
;
then
i2 < 1
+ 1
by A24, A28, A30, A31, SPRECT_3:12;
then
i2 <= 1
by NAT_1:13;
then
(Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (
i1,1)
by A28, A29, XXREAL_0:1;
hence
x in UBD (L~ (Cage (C,n)))
by A4, A12, A26, A31;
verum end; end; end; hence
x in UBD (L~ (Cage (C,n)))
;
verum end;
C c= BDD (L~ (Cage (C,n)))
by JORDAN10:12;
then
x in (BDD (L~ (Cage (C,n)))) /\ (UBD (L~ (Cage (C,n))))
by A2, A5, XBOOLE_0:def 4;
then
BDD (L~ (Cage (C,n))) meets UBD (L~ (Cage (C,n)))
;
hence
contradiction
by JORDAN2C:24; verum