let M be non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :], succ REAL ; :: thesis: ( 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 Result [x,y],M = max x,y )
assume that
A1: the carrier of M = succ REAL and
A2: the FinalS of M = REAL and
A3: the InitS of M = REAL and
A4: the OFun of M = id the carrier of M and
A5: for x, y being Real st x >= y holds
the Tran of M . [the InitS of M,[x,y]] = x and
A6: 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 Result [x,y],M = max x,y
let x, y be Real; :: thesis: Result [x,y],M = max x,y
A7: max x,y in succ REAL by XBOOLE_0:def 3;
max x,y is_result_of [x,y],M by A1, A2, A3, A4, A5, A6, Th23;
hence Result [x,y],M = max x,y by A7, Def9; :: thesis: verum