let X be set ; :: thesis: for b1, b2 being real-valued finite-support ManySortedSet of holds support (max b1,b2) c= (support b1) \/ (support b2)
let b1, b2 be real-valued finite-support ManySortedSet of ; :: thesis: support (max b1,b2) c= (support b1) \/ (support b2)
set f = max b1,b2;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (max b1,b2) or x in (support b1) \/ (support b2) )
assume x in support (max b1,b2) ; :: thesis: x in (support b1) \/ (support b2)
then A1: (max b1,b2) . x <> 0 by POLYNOM1:def 7;
( b1 . x <= b2 . x or b1 . x > b2 . x ) ;
then ( (max b1,b2) . x = b1 . x or (max b1,b2) . x = b2 . x ) by Def4;
then ( x in support b1 or x in support b2 ) by A1, POLYNOM1:def 7;
hence x in (support b1) \/ (support b2) by XBOOLE_0:def 3; :: thesis: verum