let A be non degenerated commutative Ring; :: thesis: for I1, I2 being Ideal of A
for p being prime Ideal of A holds
( not I1 *' I2 c= p or I1 c= p or I2 c= p )
let I1, I2 be Ideal of A; :: thesis: for p being prime Ideal of A holds
( not I1 *' I2 c= p or I1 c= p or I2 c= p )
let p be prime Ideal of A; :: thesis: ( not I1 *' I2 c= p or I1 c= p or I2 c= p )
( I1 c= p or I2 c= p or not I1 *' I2 c= p )

proof

assume A1: ( not I1 c= p & not I2 c= p ) ; :: thesis: not I1 *' I2 c= p
then consider x1 being object such that
A2: x1 in I1 and
A3: not x1 in p ;
consider x2 being object such that
A4: x2 in I2 and
A5: not x2 in p by A1;
reconsider x1 = x1 as Element of A by A2;
reconsider x2 = x2 as Element of A by A4;
reconsider x = x1 * x2 as Element of the carrier of A ;
reconsider seq = <*x*> as FinSequence of the carrier of A ;
A6: Sum seq = x by BINOM:3;
A8: for i being Element of NAT st 1 <= i & i <= len seq holds
ex a, b being Element of A st
( seq . i = a * b & a in I1 & b in I2 )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len seq implies ex a, b being Element of A st
( seq . i = a * b & a in I1 & b in I2 ) )
assume that
A9: 1 <= i and
A10: i <= len seq ; :: thesis: ex a, b being Element of A st
( seq . i = a * b & a in I1 & b in I2 )
A11: i <= 1 by A10, FINSEQ_1:40;
seq . i = seq . 1 by A9, XXREAL_0:1, A11
.= x1 * x2 by FINSEQ_1:40 ;
hence ex a, b being Element of A st
( seq . i = a * b & a in I1 & b in I2 ) by A2, A4; :: thesis: verum

end;

A12: Sum seq in { (Sum s) where s is FinSequence of the carrier of A : for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of A st
( s . i = a * b & a in I1 & b in I2 ) } by A8;
x1 * x2 in I1 *' I2 by A6, A12, IDEAL_1:def 21;
hence not I1 *' I2 c= p by A3, A5, RING_1:def 1; :: thesis: verum

end;

hence ( not I1 *' I2 c= p or I1 c= p or I2 c= p ) ; :: thesis: verum