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

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