consider f being BinOp of REAL such that
A1: for x, y being Real holds f . x,y = min x,y from BINOP_1:sch 4();
let M be non empty Moore-SM_Final of [:REAL ,REAL :], succ REAL ; :: thesis: ( 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 ) implies for x, y being Element of REAL holds min x,y is_result_of [x,y],M )
assume A2: ( 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 ) ; :: thesis: ( ex x, y being Real st
( x < y & not the Tran of M . [the InitS of M,[x,y]] = x ) or ex x, y being Real st
( x >= y & not the Tran of M . [the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds min x,y is_result_of [x,y],M )
assume A3: ( ( 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 ) ) ; :: thesis: for x, y being Element of REAL holds min x,y is_result_of [x,y],M
let x, y be Real; :: thesis: min x,y is_result_of [x,y],M

now

let x, y be Real; :: thesis: the Tran of M . [the InitS of M,[x,y]] = f . x,y
( ( x < y implies the Tran of M . [the InitS of M,[x,y]] = x ) & ( x >= y implies the Tran of M . [the InitS of M,[x,y]] = y ) ) by A3;
then the Tran of M . [the InitS of M,[x,y]] = min x,y by XXREAL_0:def 9;
hence the Tran of M . [the InitS of M,[x,y]] = f . x,y by A1; :: thesis: verum

end;

then f . x,y is_result_of [x,y],M by A2, Th22;
hence min x,y is_result_of [x,y],M by A1; :: thesis: verum