let A be non degenerated commutative Ring; :: thesis:
let G be Subset-Family of (Spectrum A); :: thesis:
assume A1: for S being set st S in G holds
ex E being non empty Subset of A st S = PrimeIdeals (A,E) ; :: thesis:

per cases ;

suppose A2: G <> {} ; :: thesis:

then consider o being object such that
A3: o in G by XBOOLE_0:def 1;
reconsider o = o as set by A3;
consider E being non empty Subset of A such that
A4: o = PrimeIdeals (A,E) by A1, A3;
A5: meet G = Intersect G by A2, SETFAM_1:def 9;
defpred S₁[ set ] means ex Z being non empty Subset of A st
( $1 = Z & ex D being set st
( D in G & D = PrimeIdeals (A,Z) ) );
consider SFE being set such that
A6: for x being set holds
( x in SFE iff ( x in bool the carrier of A & S₁[x] ) ) from XFAMILY:sch 1();
SFE c= bool the carrier of A by A6;
then reconsider SFE = SFE as non empty Subset-Family of the carrier of A by A3, A4, A6;
E c= union SFE by ZFMISC_1:74, A3, A4, A6;
then A8: union SFE is non empty Subset of A ;
A9: for x being object st x in Intersect G holds
x in PrimeIdeals (A,(union SFE))

proof

let x be object ; :: thesis:
assume A10: x in Intersect G ; :: thesis:
then A11: x in meet G by A2, SETFAM_1:def 9;
reconsider x = x as prime Ideal of A by A10, Th22;
union SFE c= x

proof

let o1 be object ; :: according to TARSKI:def 3 :: thesis:
assume o1 in union SFE ; :: thesis:
then consider Y being set such that
A13: o1 in Y and
A14: Y in SFE by TARSKI:def 4;
consider Z being non empty Subset of A such that
A15: Z = Y and
A16: ex D being set st
( D in G & D = PrimeIdeals (A,Z) ) by A6, A14;
consider D being set such that
A17: D in G and
A18: D = PrimeIdeals (A,Z) by A16;
x in D by A17, A11, SETFAM_1:def 1;
then consider x1 being prime Ideal of A such that
A19: x1 = x and
A20: Z c= x1 by A18;
thus o1 in x by A13, A15, A20, A19; :: thesis:

end;

hence x in PrimeIdeals (A,(union SFE)) ; :: thesis:

end;

for x being object st x in PrimeIdeals (A,(union SFE)) holds
x in Intersect G

proof

let x be object ; :: thesis:
assume A23: x in PrimeIdeals (A,(union SFE)) ; :: thesis:
for Y being set st Y in G holds
x in Y

proof

let Y be set ; :: thesis:
assume A24: Y in G ; :: thesis:
then consider E being non empty Subset of A such that
A25: Y = PrimeIdeals (A,E) by A1;
E c= union SFE by A6, A24, A25, ZFMISC_1:74;
then PrimeIdeals (A,(union SFE)) c= PrimeIdeals (A,E) by Th38;
hence x in Y by A25, A23; :: thesis:

end;

hence x in Intersect G by A2, A5, SETFAM_1:def 1; :: thesis:

end;

hence ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F) by A8, A9, TARSKI:2; :: thesis:

end;

suppose G = {} ; :: thesis:

then Intersect G = Spectrum A by SETFAM_1:def 9;
hence ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F) by Th42; :: thesis:

end;

end;