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 <= 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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:36, 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;