let A be non degenerated commutative Ring; :: thesis: for G being Subset-Family of (Spectrum A) st ( for S being set st S in G holds
ex E being non empty Subset of A st S = PrimeIdeals (A,E) ) holds
ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F)
let G be Subset-Family of (Spectrum A); :: thesis: ( ( for S being set st S in G holds
ex E being non empty Subset of A st S = PrimeIdeals (A,E) ) implies ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F) )
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: ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F)

per cases ( G <> {} or G = {} ) ;

suppose A2: G <> {} ; :: thesis: ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F)

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: ( x in Intersect G implies x in PrimeIdeals (A,(union SFE)) )
assume A10: x in Intersect G ; :: thesis: x in PrimeIdeals (A,(union SFE))
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: ( not o1 in union SFE or o1 in x )
assume o1 in union SFE ; :: thesis: o1 in x
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: verum

end;

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

end;

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

proof

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

proof

let Y be set ; :: thesis: ( Y in G implies x in Y )
assume A24: Y in G ; :: thesis: x in Y
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: verum

end;

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

end;

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

end;

suppose G = {} ; :: thesis: ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F)

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: verum

end;

end;