for a being set holds
( a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) iff a = |[0 ,0 ]| )
proof
let a be
set ;
( a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) iff a = |[0 ,0 ]| )
thus
(
a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) implies
a = |[0 ,0 ]| )
( a = |[0 ,0 ]| implies a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) )proof
assume A1:
a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
;
a = |[0 ,0 ]|
then
a in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) }
by Th19, XBOOLE_0:def 4;
then A2:
ex
p2 being
Point of
(TOP-REAL 2) st
(
p2 = a &
p2 `1 <= 1 &
p2 `1 >= 0 &
p2 `2 = 0 )
;
a in LSeg |[0 ,0 ]|,
|[0 ,1]|
by A1, XBOOLE_0:def 4;
then
ex
p being
Point of
(TOP-REAL 2) st
(
p = a &
p `1 = 0 &
p `2 <= 1 &
p `2 >= 0 )
by Th19;
hence
a = |[0 ,0 ]|
by A2, EUCLID:57;
verum
end;
assume A3:
a = |[0 ,0 ]|
;
a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
then A4:
a in LSeg |[0 ,0 ]|,
|[1,0 ]|
by RLTOPSP1:69;
a in LSeg |[0 ,0 ]|,
|[0 ,1]|
by A3, RLTOPSP1:69;
hence
a in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
by A4, XBOOLE_0:def 4;
verum
end;
hence
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,0 ]|}
by TARSKI:def 1; verum