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 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 (TOP-REAL 2) ;

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 A2, PSCOMP_1:24;

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:11;

then A7: ((Gauge (E,0)) * (2,1)) `1 <= x `1 by A2, PSCOMP_1:24;

A8: (len (Gauge (E,0))) -' 1 = 3 by Lm1;

then ((Gauge (E,0)) * ((2 + 1),1)) `1 = E-bound E by A4, JORDAN8:12;

then A9: x `1 <= ((Gauge (E,0)) * ((2 + 1),1)) `1 by A2, PSCOMP_1:24;

((Gauge (E,0)) * (1,(2 + 1))) `2 = N-bound E by A8, A4, JORDAN8:14;

then A10: x `2 <= ((Gauge (E,0)) * (1,(2 + 1))) `2 by A2, PSCOMP_1:24;

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

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 (TOP-REAL 2) ;

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 A2, PSCOMP_1:24;

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:11;

then A7: ((Gauge (E,0)) * (2,1)) `1 <= x `1 by A2, PSCOMP_1:24;

A8: (len (Gauge (E,0))) -' 1 = 3 by Lm1;

then ((Gauge (E,0)) * ((2 + 1),1)) `1 = E-bound E by A4, JORDAN8:12;

then A9: x `1 <= ((Gauge (E,0)) * ((2 + 1),1)) `1 by A2, PSCOMP_1:24;

((Gauge (E,0)) * (1,(2 + 1))) `2 = N-bound E by A8, A4, JORDAN8:14;

then A10: x `2 <= ((Gauge (E,0)) * (1,(2 + 1))) `2 by A2, PSCOMP_1:24;

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