let
s
,
r
be
Real
;
:: thesis:
(
r
<=
s
implies (
r
<=
(
r
+
s
)
/
2 &
(
r
+
s
)
/
2
<=
s
) )
assume
A1
:
r
<=
s
;
:: thesis:
(
r
<=
(
r
+
s
)
/
2 &
(
r
+
s
)
/
2
<=
s
)
per
cases
(
r
<
s
or
r
=
s
)
by
A1
,
XXREAL_0:1
;
suppose
r
<
s
;
:: thesis:
(
r
<=
(
r
+
s
)
/
2 &
(
r
+
s
)
/
2
<=
s
)
hence
(
r
<=
(
r
+
s
)
/
2 &
(
r
+
s
)
/
2
<=
s
)
by
XREAL_1:226
;
:: thesis:
verum
end;
suppose
r
=
s
;
:: thesis:
(
r
<=
(
r
+
s
)
/
2 &
(
r
+
s
)
/
2
<=
s
)
hence
(
r
<=
(
r
+
s
)
/
2 &
(
r
+
s
)
/
2
<=
s
) ;
:: thesis:
verum
end;
end;