for a being set 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
set ;
( 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 ]| )
( 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]|)
;
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 Th19, 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 Th19;
hence
a = |[1,0 ]|
by A2, EUCLID:57;
verum
end;
assume A3:
a = |[1,0 ]|
;
a in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
then A4:
a in LSeg |[1,0 ]|,
|[1,1]|
by RLTOPSP1:69;
a in LSeg |[0 ,0 ]|,
|[1,0 ]|
by A3, RLTOPSP1:69;
hence
a in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
by A4, XBOOLE_0:def 4;
verum
end;
hence
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[1,0 ]|}
by TARSKI:def 1; verum