let a, b, c, d be Real; :: thesis: ( 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 ; :: thesis: (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|}

for ax being object holds

( ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) iff ax = |[b,c]| )

assume that

A1: a <= b and

A2: c <= d ; :: thesis: (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|}

for ax being object holds

( ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) iff ax = |[b,c]| )

proof

hence
(LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|}
by TARSKI:def 1; :: thesis: verum
let ax be object ; :: thesis: ( 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]| ) :: thesis: ( ax = |[b,c]| implies ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) )

then A8: ax in LSeg (|[a,c]|,|[b,c]|) by RLTOPSP1:68;

ax in LSeg (|[b,c]|,|[b,d]|) by A7, RLTOPSP1:68;

hence ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) by A8, XBOOLE_0:def 4; :: thesis: verum

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

proof

assume A7:
ax = |[b,c]|
; :: thesis: ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|))
assume A3:
ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|))
; :: thesis: 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, Th30;

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, Th30;

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:53; :: thesis: verum

end;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, Th30;

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, Th30;

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:53; :: thesis: verum

then A8: ax in LSeg (|[a,c]|,|[b,c]|) by RLTOPSP1:68;

ax in LSeg (|[b,c]|,|[b,d]|) by A7, RLTOPSP1:68;

hence ax in (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) by A8, XBOOLE_0:def 4; :: thesis: verum