theorem Th24:
for
M being non
empty Moore-SM_Final over
[:REAL,REAL:],
succ REAL st
M is
calculating_type & the
carrier of
M = succ REAL & the
FinalS of
M = REAL & the
InitS of
M = REAL & the
OFun of
M = id the
carrier of
M & ( for
x,
y being
Real st
x < y holds
the
Tran of
M . [ the InitS of M,[x,y]] = x ) & ( for
x,
y being
Real st
x >= y holds
the
Tran of
M . [ the InitS of M,[x,y]] = y ) holds
for
x,
y being
Element of
REAL holds
min (
x,
y)
is_result_of [x,y],
M