let T1, T2 be strict TopSpace; :: thesis: ( the carrier of T1 = Spectrum A & ( for F being Subset of T1 holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) & the carrier of T2 = Spectrum A & ( for F being Subset of T2 holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) implies T1 = T2 )
assume that
A5: the carrier of T1 = Spectrum A and
A6: for F being Subset of T1 holds
( F is closed iff ex Z1 being non empty Subset of A st F = PrimeIdeals (A,Z1) ) and
A7: the carrier of T2 = Spectrum A and
A8: for F being Subset of T2 holds
( F is closed iff ex Z2 being non empty Subset of A st F = PrimeIdeals (A,Z2) ) ; :: thesis: T1 = T2
now :: thesis: for F being set holds
( F is closed Subset of T1 iff F is closed Subset of T2 )
let F be set ; :: thesis: ( F is closed Subset of T1 iff F is closed Subset of T2 )
( F is closed Subset of T1 iff ex Z1 being non empty Subset of A st F = PrimeIdeals (A,Z1) ) by A5, A6;
hence ( F is closed Subset of T1 iff F is closed Subset of T2 ) by A7, A8; :: thesis: verum
end;
hence T1 = T2 by TOPGEN_3:6; :: thesis: verum