let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: C misses L~ (Cage (C,n))
set f = Cage (C,n);
set G = Gauge (C,n);
assume not C misses L~ (Cage (C,n)) ; :: thesis: contradiction
then consider c being object such that
A1: c in C and
A2: c in L~ (Cage (C,n)) by XBOOLE_0:3;
L~ (Cage (C,n)) = union { (LSeg ((Cage (C,n)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (Cage (C,n)) ) } by TOPREAL1:def 4;
then consider Z being set such that
A3: c in Z and
A4: Z in { (LSeg ((Cage (C,n)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (Cage (C,n)) ) } by A2, TARSKI:def 4;
consider i being Nat such that
A5: Z = LSeg ((Cage (C,n)),i) and
A6: ( 1 <= i & i + 1 <= len (Cage (C,n)) ) by A4;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then LSeg ((Cage (C,n)),i) = (left_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) by A6, GOBRD13:29;
then A7: c in left_cell ((Cage (C,n)),i,(Gauge (C,n))) by A3, A5, XBOOLE_0:def 4;
left_cell ((Cage (C,n)),i,(Gauge (C,n))) misses C by A6, JORDAN9:31;
hence contradiction by A1, A7, XBOOLE_0:3; :: thesis: verum