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 )
A1: len (Gauge E,0 ) = width (Gauge E,0 ) by JORDAN8:def 1;
assume A2: x in E ; :: thesis: x in cell (Gauge E,0 ),2,2
then reconsider x = x as Point of (TOP-REAL 2) ;
A3: 4 <= len (Gauge E,0 ) by JORDAN8:13;
then A4: 1 < len (Gauge E,0 ) by XXREAL_0:2;
then ((Gauge E,0 ) * 1,2) `2 = S-bound E by JORDAN8:16;
then A5: ((Gauge E,0 ) * 1,2) `2 <= x `2 by A2, PSCOMP_1:71;
2 < len (Gauge E,0 ) by A3, XXREAL_0:2;
then A6: 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 A1, GOBRD11:32;
((Gauge E,0 ) * 2,1) `1 = W-bound E by A4, JORDAN8:14;
then A7: ((Gauge E,0 ) * 2,1) `1 <= x `1 by A2, PSCOMP_1:71;
A8: (len (Gauge E,0 )) -' 1 = 3 by Lm1;
then ((Gauge E,0 ) * (2 + 1),1) `1 = E-bound E by A4, JORDAN8:15;
then A9: x `1 <= ((Gauge E,0 ) * (2 + 1),1) `1 by A2, PSCOMP_1:71;
((Gauge E,0 ) * 1,(2 + 1)) `2 = N-bound E by A8, A4, JORDAN8:17;
then A10: x `2 <= ((Gauge E,0 ) * 1,(2 + 1)) `2 by A2, PSCOMP_1:71;
x = |[(x `1 ),(x `2 )]| by EUCLID:57;
hence x in cell (Gauge E,0 ),2,2 by A7, A9, A5, A10, A6; :: thesis: verum