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