let E be compact non horizontal non vertical Subset of (TOP-REAL 2); E c= cell ((Gauge (E,0)),2,2)
set G = Gauge (E,0);
let x be object ; TARSKI:def 3 ( 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
; 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; verum