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