let E be compact non horizontal non vertical Subset of (); :: thesis: E c= cell ((Gauge (E,0)),2,2)
set G = Gauge (E,0);
let x be object ; :: 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 () ;
A3: 4 <= len (Gauge (E,0)) by JORDAN8:10;
then A4: 1 < len (Gauge (E,0)) by XXREAL_0:2;
then ((Gauge (E,0)) * (1,2)) `2 = S-bound E by JORDAN8:13;
then A5: ((Gauge (E,0)) * (1,2)) `2 <= x `2 by ;
2 < len (Gauge (E,0)) by ;
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 ;
((Gauge (E,0)) * (2,1)) `1 = W-bound E by ;
then A7: ((Gauge (E,0)) * (2,1)) `1 <= x `1 by ;
A8: (len (Gauge (E,0))) -' 1 = 3 by Lm1;
then ((Gauge (E,0)) * ((2 + 1),1)) `1 = E-bound E by ;
then A9: x `1 <= ((Gauge (E,0)) * ((2 + 1),1)) `1 by ;
((Gauge (E,0)) * (1,(2 + 1))) `2 = N-bound E by ;
then A10: x `2 <= ((Gauge (E,0)) * (1,(2 + 1))) `2 by ;
x = |[(x `1),(x `2)]| by EUCLID:53;
hence x in cell ((Gauge (E,0)),2,2) by A7, A9, A5, A10, A6; :: thesis: verum