let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|} )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|}
for ax being set holds
( ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) iff ax = |[a,d]| )

proof

let ax be set ; :: thesis: ( ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) iff ax = |[a,d]| )
thus ( ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) implies ax = |[a,d]| ) :: thesis: ( ax = |[a,d]| implies ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) )

proof

assume A3: ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) ; :: thesis: ax = |[a,d]|
then A4: ax in LSeg |[a,c]|,|[a,d]| by XBOOLE_0:def 4;
ax in LSeg |[a,d]|,|[b,d]| 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 = d ) } by A1, Th39;
then A5: ex p2 being Point of (TOP-REAL 2) st
( p2 = ax & p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) ;
ax in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = a & p2 `2 <= d & p2 `2 >= c ) } by A2, A4, Th39;
then ex p being Point of (TOP-REAL 2) st
( p = ax & p `1 = a & p `2 <= d & p `2 >= c ) ;
hence ax = |[a,d]| by A5, EUCLID:57; :: thesis: verum

end;

assume A6: ax = |[a,d]| ; :: thesis: ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|)
then A7: ax in LSeg |[a,c]|,|[a,d]| by RLTOPSP1:69;
ax in LSeg |[a,d]|,|[b,d]| by A6, RLTOPSP1:69;
hence ax in (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) by A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|} by TARSKI:def 1; :: thesis: verum