let n be Nat; :: thesis: 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); :: thesis: 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 k, t being Nat such that
A1: 1 <= k and
A2: k <= len (Cage (C,n)) and
A3: ( 1 <= t & t <= len (Gauge (C,n)) ) and
A4: (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) by Lm16;

per cases ( k < len (Cage (C,n)) or k = len (Cage (C,n)) ) by A2, XXREAL_0:1;

suppose k < len (Cage (C,n)) ; :: thesis: 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) )

hence 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) ) by A1, A3, A4; :: thesis: verum

end;

suppose A5: k = len (Cage (C,n)) ; :: thesis: 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) )

take 1 ; :: thesis: ex t being Nat st
( 1 <= 1 & 1 < len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. 1 = (Gauge (C,n)) * (t,1) )
take t ; :: thesis: ( 1 <= 1 & 1 < len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. 1 = (Gauge (C,n)) * (t,1) )
thus ( 1 <= 1 & 1 < len (Cage (C,n)) ) by GOBOARD7:34, XXREAL_0:2; :: thesis: ( 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. 1 = (Gauge (C,n)) * (t,1) )
thus ( 1 <= t & t <= len (Gauge (C,n)) ) by A3; :: thesis: (Cage (C,n)) /. 1 = (Gauge (C,n)) * (t,1)
thus (Cage (C,n)) /. 1 = (Gauge (C,n)) * (t,1) by A4, A5, FINSEQ_6:def 1; :: thesis: verum

end;

end;