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 object 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 Th23;
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 Th26;
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, Th15; :: thesis: verum