let D2 be non empty compact non horizontal Subset of (TOP-REAL 2); 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))) <> {}
; XBOOLE_0:def 7 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; verum