let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: not cell ((Gauge (E,0)),2,2) c= BDD E

assume A1: cell ((Gauge (E,0)),2,2) c= BDD E ; :: thesis: contradiction

E c= cell ((Gauge (E,0)),2,2) by Th17;

then A2: E c= BDD E by A1;

set e = the Element of E;

A3: BDD E misses E by JORDAN1A:7;

the Element of E in E ;

hence contradiction by A2, A3, XBOOLE_0:3; :: thesis: verum

assume A1: cell ((Gauge (E,0)),2,2) c= BDD E ; :: thesis: contradiction

E c= cell ((Gauge (E,0)),2,2) by Th17;

then A2: E c= BDD E by A1;

set e = the Element of E;

A3: BDD E misses E by JORDAN1A:7;

the Element of E in E ;

hence contradiction by A2, A3, XBOOLE_0:3; :: thesis: verum