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