let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: E c= cell (Gauge E,0 ),2,2
set G = Gauge E,0 ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in E or x in cell (Gauge E,0 ),2,2 )
assume A1: x in E ; :: thesis: x in cell (Gauge E,0 ),2,2
then reconsider x = x as Point of (TOP-REAL 2) ;
A2: x = |[(x `1 ),(x `2 )]| by EUCLID:57;
A3: len (Gauge E,0 ) = width (Gauge E,0 ) by JORDAN8:def 1;
A4: (len (Gauge E,0 )) -' 1 = 3 by Lm1;
A5: 4 <= len (Gauge E,0 ) by JORDAN8:13;
then 1 < len (Gauge E,0 ) by XXREAL_0:2;
then ( ((Gauge E,0 ) * (2 + 1),1) `1 = E-bound E & ((Gauge E,0 ) * 1,2) `2 = S-bound E & ((Gauge E,0 ) * 1,(2 + 1)) `2 = N-bound E & ((Gauge E,0 ) * 2,1) `1 = W-bound E ) by A4, JORDAN8:14, JORDAN8:15, JORDAN8:16, JORDAN8:17;
then A6: ( ((Gauge E,0 ) * 2,1) `1 <= x `1 & x `1 <= ((Gauge E,0 ) * (2 + 1),1) `1 & ((Gauge E,0 ) * 1,2) `2 <= x `2 & x `2 <= ((Gauge E,0 ) * 1,(2 + 1)) `2 ) by A1, PSCOMP_1:71;
2 < len (Gauge E,0 ) by A5, XXREAL_0:2;
then cell (Gauge E,0 ),2,2 = { |[p,q]| where p, q is Real : ( ((Gauge E,0 ) * 2,1) `1 <= p & p <= ((Gauge E,0 ) * (2 + 1),1) `1 & ((Gauge E,0 ) * 1,2) `2 <= q & q <= ((Gauge E,0 ) * 1,(2 + 1)) `2 ) } by A3, GOBRD11:32;
hence x in cell (Gauge E,0 ),2,2 by A2, A6; :: thesis: verum