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