let A be non degenerated commutative Ring; for E1, E2 being non empty Subset of A ex E3 being non empty Subset of A st (PrimeIdeals (A,E1)) \/ (PrimeIdeals (A,E2)) = PrimeIdeals (A,E3)
let E1, E2 be non empty Subset of A; ex E3 being non empty Subset of A st (PrimeIdeals (A,E1)) \/ (PrimeIdeals (A,E2)) = PrimeIdeals (A,E3)
set F1 = PrimeIdeals (A,E1);
set F2 = PrimeIdeals (A,E2);
set I1 = E1 -Ideal ;
set I2 = E2 -Ideal ;
reconsider I3 = (E1 -Ideal) *' (E2 -Ideal) as Ideal of A ;
A4:
PrimeIdeals (A,E1) = PrimeIdeals (A,(E1 -Ideal))
by Th34;
A5:
PrimeIdeals (A,I3) c= (PrimeIdeals (A,(E1 -Ideal))) \/ (PrimeIdeals (A,(E2 -Ideal)))
proof
let x be
object ;
TARSKI:def 3 ( not x in PrimeIdeals (A,I3) or x in (PrimeIdeals (A,(E1 -Ideal))) \/ (PrimeIdeals (A,(E2 -Ideal))) )
assume
x in PrimeIdeals (
A,
I3)
;
x in (PrimeIdeals (A,(E1 -Ideal))) \/ (PrimeIdeals (A,(E2 -Ideal)))
then consider x1 being
prime Ideal of
A such that A7:
x1 = x
and A8:
I3 c= x1
;
A9:
(
E1 -Ideal c= x1 or
E2 -Ideal c= x1 )
by A8, Th40;
(
x1 in { p where p is prime Ideal of A : E1 -Ideal c= p } or
x1 in { p where p is prime Ideal of A : E2 -Ideal c= p } )
by A9;
hence
x in (PrimeIdeals (A,(E1 -Ideal))) \/ (PrimeIdeals (A,(E2 -Ideal)))
by A7, XBOOLE_0:def 3;
verum
end;
A11:
(PrimeIdeals (A,(E1 -Ideal))) \/ (PrimeIdeals (A,(E2 -Ideal))) c= PrimeIdeals (A,I3)
PrimeIdeals (A,I3) = (PrimeIdeals (A,E1)) \/ (PrimeIdeals (A,E2))
by A4, A5, A11, Th34;
hence
ex E3 being non empty Subset of A st (PrimeIdeals (A,E1)) \/ (PrimeIdeals (A,E2)) = PrimeIdeals (A,E3)
; verum