let
t
,
p
,
s
be
Real
;
:: thesis:
(
0
<
s
&
t
<=
p
implies (
t
<
p
+
s
&
t

s
<
p
) )
assume
(
0
<
s
&
t
<=
p
) ;
:: thesis:
(
t
<
p
+
s
&
t

s
<
p
)
then
t
+
0
<
p
+
s
by
XREAL_1:8
;
hence
(
t
<
p
+
s
&
t

s
<
p
)
by
XREAL_1:19
;
:: thesis:
verum