let A be non degenerated commutative Ring; :: thesis: for a, b being Ideal of A
for p being prime Ideal of A holds
( not a /\ b c= p or a c= p or b c= p )
let a, b be Ideal of A; :: thesis: for p being prime Ideal of A holds
( not a /\ b c= p or a c= p or b c= p )
let p be prime Ideal of A; :: thesis: ( not a /\ b c= p or a c= p or b c= p )
assume A1: a /\ b c= p ; :: thesis: ( a c= p or b c= p )
a *' b c= a /\ b by IDEAL_1:79;
then a *' b c= p by A1;
hence ( a c= p or b c= p ) by TOPZARI1:30; :: thesis: verum