let
s
,
t
be
Real
;
:: thesis:
(
s
<=
t
implies

t
<=

s
)
assume
s
<=
t
;
:: thesis:

t
<=

s
then
s

t
<=
t

t
by
Lm5
;
then
(
s

t
)

s
<=
0

s
by
Lm5
;
hence

t
<=

s
;
:: thesis:
verum