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) * 1,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) * 1,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) * 1,t ) by Lm15;

per cases ( k < len (Cage C,n) or k = len (Cage C,n) ) by A1, 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 <= width (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * 1,t )

hence 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) * 1,t ) by A1; :: thesis: verum

end;

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) * 1,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) * 1,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) * 1,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) * 1,t )
thus ( 1 <= t & t <= width (Gauge C,n) ) by A1; :: thesis: (Cage C,n) /. 1 = (Gauge C,n) * 1,t
thus (Cage C,n) /. 1 = (Gauge C,n) * 1,t by A1, A2, FINSEQ_6:def 1; :: thesis: verum

end;

end;