let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i, j, n being Nat st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i <> 0
let i, j, n be Nat; ( j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i <> 0 )
assume that
A1:
j <= width (Gauge (C,n))
and
A2:
cell ((Gauge (C,n)),i,j) c= BDD C
and
A3:
i = 0
; contradiction
A4:
cell ((Gauge (C,n)),0,j) c= UBD C
by A1, Th35;
0 <= len (Gauge (C,n))
;
then
not cell ((Gauge (C,n)),0,j) is empty
by A1, JORDAN1A:24;
hence
contradiction
by A2, A3, A4, JORDAN2C:24, XBOOLE_1:68; verum