defpred S₁[ set ] means ex Z being non empty Subset of A st $1 = PrimeIdeals (A,Z);
A1: for F1, F2 being set st S₁[F1] & S₁[F2] holds
S₁[F1 \/ F2] by Th43;
A2: for G being Subset-Family of (Spectrum A) st ( for S being set st S in G holds
S₁[S] ) holds
S₁[ Intersect G] by Th44;
A3: ( S₁[ {} ] & S₁[ Spectrum A] ) by Th41, Th42;
consider T being strict TopSpace such that
A4: ( the carrier of T = Spectrum A & ( for E being Subset of T holds
( E is closed iff S₁[E] ) ) ) from TOPGEN_3:sch 1(A3, A1, A2);
take T ; :: thesis: ( the carrier of T = Spectrum A & ( for F being Subset of T holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) )
thus the carrier of T = Spectrum A by A4; :: thesis: for F being Subset of T holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) )
let F be Subset of T; :: thesis: ( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) )
thus ( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) by A4; :: thesis: verum