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