let X be set ; :: thesis: for b1, b2 being bag of X holds support (min b1,b2) = (support b1) /\ (support b2)
let b1, b2 be bag of X; :: thesis: support (min b1,b2) = (support b1) /\ (support b2)
set f = min b1,b2;
A1: for x being set st x in support (min b1,b2) holds
( x in support b1 & x in support b2 )

proof

let x be set ; :: thesis: ( x in support (min b1,b2) implies ( x in support b1 & x in support b2 ) )
assume A2: x in support (min b1,b2) ; :: thesis: ( x in support b1 & x in support b2 )
assume A3: ( not x in support b1 or not x in support b2 ) ; :: thesis: contradiction

now

per cases ( b1 . x <= b2 . x or b2 . x < b1 . x ) ;

case A4: b1 . x <= b2 . x ; :: thesis: contradiction

A5: not x in support b1

proof

assume A6: x in support b1 ; :: thesis: contradiction
then A7: b1 . x <> 0 by PRE_POLY:def 7;
b2 . x = 0 by A3, A6, PRE_POLY:def 7;
hence contradiction by A4, A7; :: thesis: verum

end;

(min b1,b2) . x = b1 . x by A4, NAT_3:def 3
.= 0 by A5, PRE_POLY:def 7 ;
hence contradiction by A2, PRE_POLY:def 7; :: thesis: verum

end;

case A8: b2 . x < b1 . x ; :: thesis: contradiction

then (min b1,b2) . x = b2 . x by NAT_3:def 3
.= 0 by A3, A8, PRE_POLY:def 7 ;
hence contradiction by A2, PRE_POLY:def 7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

for x being set st x in support b1 & x in support b2 holds
x in support (min b1,b2)

proof

let x be set ; :: thesis: ( x in support b1 & x in support b2 implies x in support (min b1,b2) )
assume that
A9: x in support b1 and
A10: x in support b2 ; :: thesis: x in support (min b1,b2)
A11: b2 . x <> 0 by A10, PRE_POLY:def 7;
( b1 . x <= b2 . x or b1 . x > b2 . x ) ;
then A12: ( (min b1,b2) . x = b1 . x or (min b1,b2) . x = b2 . x ) by NAT_3:def 3;
b1 . x <> 0 by A9, PRE_POLY:def 7;
hence x in support (min b1,b2) by A11, A12, PRE_POLY:def 7; :: thesis: verum

end;

hence support (min b1,b2) = (support b1) /\ (support b2) by A1, XBOOLE_0:def 4; :: thesis: verum