let a, b, c, d be Real; ( a <= b & c <= d implies (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|} )
assume that
A1:
a <= b
and
A2:
c <= d
; (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|}
for ax being object holds
( ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) iff ax = |[a,c]| )
proof
let ax be
object ;
( ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) iff ax = |[a,c]| )
thus
(
ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) implies
ax = |[a,c]| )
( ax = |[a,c]| implies ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) )proof
assume A3:
ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|))
;
ax = |[a,c]|
then A4:
ax in LSeg (
|[a,c]|,
|[a,d]|)
by XBOOLE_0:def 4;
ax in LSeg (
|[a,c]|,
|[b,c]|)
by A3, XBOOLE_0:def 4;
then
ax in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) }
by A1, Th30;
then A5:
ex
p2 being
Point of
(TOP-REAL 2) st
(
p2 = ax &
p2 `1 <= b &
p2 `1 >= a &
p2 `2 = c )
;
ax in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = a & p2 `2 <= d & p2 `2 >= c ) }
by A2, A4, Th30;
then
ex
p being
Point of
(TOP-REAL 2) st
(
p = ax &
p `1 = a &
p `2 <= d &
p `2 >= c )
;
hence
ax = |[a,c]|
by A5, EUCLID:53;
verum
end;
assume A6:
ax = |[a,c]|
;
ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|))
then A7:
ax in LSeg (
|[a,c]|,
|[a,d]|)
by RLTOPSP1:68;
ax in LSeg (
|[a,c]|,
|[b,c]|)
by A6, RLTOPSP1:68;
hence
ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|))
by A7, XBOOLE_0:def 4;
verum
end;
hence
(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|}
by TARSKI:def 1; verum