set f = max b1,b2;
let x be set ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom (max b1,b2) or (max b1,b2) . x is natural )
assume x in dom (max b1,b2) ; :: thesis: (max b1,b2) . x is natural
( b1 . x <= b2 . x or b1 . x > b2 . x ) ;
hence (max b1,b2) . x is natural by Def4; :: thesis: verum