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