let n be set ; :: thesis: for a, b being bag of n st b divides a holds
support b c= support a
let a, b be bag of n; :: thesis: ( b divides a implies support b c= support a )
assume A1: b divides a ; :: thesis: support b c= support a
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support b or x in support a )
assume x in support b ; :: thesis: x in support a
then b . x <> 0 by PRE_POLY:def 7;
then a . x <> 0 by A1, PRE_POLY:def 11;
hence x in support a by PRE_POLY:def 7; :: thesis: verum