for a being object holds
( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,0]| )

proof

set p00 = |[0,0]|;
set p10 = |[1,0]|;
set p11 = |[1,1]|;
let a be object ; :: thesis: ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,0]| )
thus ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies a = |[1,0]| ) :: thesis: ( a = |[1,0]| implies a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) )

proof

assume A1: a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: a = |[1,0]|
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by Th13, XBOOLE_0:def 4;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ;
a in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def 4;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = a & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13;
hence a = |[1,0]| by A2, EUCLID:53; :: thesis: verum

end;

assume A3: a = |[1,0]| ; :: thesis: a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
then A4: a in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68;
a in LSeg (|[0,0]|,|[1,0]|) by A3, RLTOPSP1:68;
hence a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

hence (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|} by TARSKI:def 1; :: thesis: verum