let D1 be non empty compact non vertical Subset of (TOP-REAL 2); :: thesis: LSeg (SW-corner D1),(NW-corner D1) misses LSeg (SE-corner D1),(NE-corner D1)
assume (LSeg (SW-corner D1),(NW-corner D1)) /\ (LSeg (SE-corner D1),(NE-corner D1)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider a being set such that
A1: a in (LSeg (SW-corner D1),(NW-corner D1)) /\ (LSeg (SE-corner D1),(NE-corner D1)) by XBOOLE_0:def 1;
a in LSeg (NE-corner D1),(SE-corner D1) by A1, XBOOLE_0:def 4;
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 ) } by Th25;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = E-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 ) ;
a in LSeg (NW-corner D1),(SW-corner D1) by A1, XBOOLE_0:def 4;
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 ) } by Th28;
then ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = W-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 ) ;
hence contradiction by A2, Th17; :: thesis: verum