let a, b, c, d be Real; :: thesis: ( 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 ; :: thesis: (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 ; :: thesis: ( 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]| ) :: thesis: ( 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]|)) ; :: thesis: 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 ;
then ax in { p2 where p2 is Point of () : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) } by ;
then A5: ex p2 being Point of () st
( p2 = ax & p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) ;
ax in { p2 where p2 is Point of () : ( p2 `1 = a & p2 `2 <= d & p2 `2 >= c ) } by A2, A4, Th30;
then ex p being Point of () st
( p = ax & p `1 = a & p `2 <= d & p `2 >= c ) ;
hence ax = |[a,c]| by ; :: thesis: verum
end;
assume A6: ax = |[a,c]| ; :: thesis: 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 ;
hence ax in (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) by ; :: thesis: verum
end;
hence (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|} by TARSKI:def 1; :: thesis: verum