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

proof

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

proof

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

end;

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

end;

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