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