consider x being Element of (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|);
assume (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A1: ( x in LSeg |[1,0 ]|,|[1,1]| & x in LSeg |[0 ,0 ]|,|[0 ,1]| ) by XBOOLE_0:def 4;
then A2: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) by Th19;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by A1, Th19;
hence contradiction by A2; :: thesis: verum