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