for a being object holds
( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) iff a = |[0,0]| )
proof
let a be
object ;
( 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 Th13, 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 Th13;
hence
a = |[0,0]|
by A2, EUCLID:53;
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:68;
a in LSeg (
|[0,0]|,
|[0,1]|)
by A3, RLTOPSP1:68;
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