let A be non degenerated commutative Ring; :: thesis: for E1, E2 being Subset of A st E2 c= E1 holds
PrimeIdeals (A,E1) c= PrimeIdeals (A,E2)
let E1, E2 be Subset of A; :: thesis: ( E2 c= E1 implies PrimeIdeals (A,E1) c= PrimeIdeals (A,E2) )
assume A1: E2 c= E1 ; :: thesis: PrimeIdeals (A,E1) c= PrimeIdeals (A,E2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeIdeals (A,E1) or x in PrimeIdeals (A,E2) )
assume x in PrimeIdeals (A,E1) ; :: thesis: x in PrimeIdeals (A,E2)
then consider x1 being prime Ideal of A such that
A3: x1 = x and
A4: E1 c= x1 ;
E2 c= x1 by A1, A4;
hence x in PrimeIdeals (A,E2) by A3; :: thesis: verum