let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st
( 1 <= k & k < len (Cage C,n) & 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (len (Gauge C,n)),t )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex k, t being Element of NAT st
( 1 <= k & k < len (Cage C,n) & 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (len (Gauge C,n)),t )
consider k, t being Element of NAT such that
A1:
( 1 <= k & k <= len (Cage C,n) & 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (len (Gauge C,n)),t )
by Lm17;
per cases
( k < len (Cage C,n) or k = len (Cage C,n) )
by A1, XXREAL_0:1;
suppose A2:
k = len (Cage C,n)
;
:: thesis: ex k, t being Element of NAT st
( 1 <= k & k < len (Cage C,n) & 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (len (Gauge C,n)),t )take
1
;
:: thesis: ex t being Element of NAT st
( 1 <= 1 & 1 < len (Cage C,n) & 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. 1 = (Gauge C,n) * (len (Gauge C,n)),t )take
t
;
:: thesis: ( 1 <= 1 & 1 < len (Cage C,n) & 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. 1 = (Gauge C,n) * (len (Gauge C,n)),t )thus
( 1
<= 1 & 1
< len (Cage C,n) )
by GOBOARD7:36, XXREAL_0:2;
:: thesis: ( 1 <= t & t <= width (Gauge C,n) & (Cage C,n) /. 1 = (Gauge C,n) * (len (Gauge C,n)),t )thus
( 1
<= t &
t <= width (Gauge C,n) )
by A1;
:: thesis: (Cage C,n) /. 1 = (Gauge C,n) * (len (Gauge C,n)),tthus
(Cage C,n) /. 1
= (Gauge C,n) * (len (Gauge C,n)),
t
by A1, A2, FINSEQ_6:def 1;
:: thesis: verum end;