let n be Element of 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 set 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 Element of NAT : ( 1 <= i & i + 1 <= len (Cage C,n) ) } by TOPREAL1:def 6;
then consider Z being set such that
A3: c in Z and
A4: Z in { (LSeg (Cage C,n),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Cage C,n) ) } by A2, TARSKI:def 4;
consider i being Element of 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:30;
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:33;
hence contradiction by A1, A7, XBOOLE_0:3; :: thesis: verum