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

proof

let x be object ; :: thesis:
assume A2: x in support (min (b1,b2)) ; :: thesis:
assume A3: ( not x in support b1 or not x in support b2 ) ; :: thesis:

now :: thesis:

per cases ;

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

A5: not x in support b1

proof

assume A6: x in support b1 ; :: thesis:
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:

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:

end;

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

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:

end;

end;

end;

hence contradiction ; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume that
A9: x in support b1 and
A10: x in support b2 ; :: thesis:
A11: b2 . x <> 0 by A10, PRE_POLY:def 7;
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:

end;

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