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 <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )
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 <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )
consider k, t being Nat such that
A1:
1 <= k
and
A2:
k <= len (Cage (C,n))
and
A3:
( 1 <= t & t <= width (Gauge (C,n)) )
and
A4:
(Cage (C,n)) /. k = (Gauge (C,n)) * (1,t)
by Lm15;
per cases
( k < len (Cage (C,n)) or k = len (Cage (C,n)) )
by A2, XXREAL_0:1;
suppose A5:
k = len (Cage (C,n))
;
ex k, t being Nat st
( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )take
1
;
ex t being Nat st
( 1 <= 1 & 1 < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. 1 = (Gauge (C,n)) * (1,t) )take
t
;
( 1 <= 1 & 1 < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. 1 = (Gauge (C,n)) * (1,t) )thus
( 1
<= 1 & 1
< len (Cage (C,n)) )
by GOBOARD7:34, XXREAL_0:2;
( 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. 1 = (Gauge (C,n)) * (1,t) )thus
( 1
<= t &
t <= width (Gauge (C,n)) )
by A3;
(Cage (C,n)) /. 1 = (Gauge (C,n)) * (1,t)thus
(Cage (C,n)) /. 1
= (Gauge (C,n)) * (1,
t)
by A4, A5, FINSEQ_6:def 1;
verum end; end;