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