let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
let E be Subset of X; :: thesis: for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
let F be Subset of X0; :: thesis: ( F = E implies (Stone-retraction (X,X0)) " F = MaxADSet E )
assume A1: F = E ; :: thesis: (Stone-retraction (X,X0)) " F = MaxADSet E
Stone-retraction (X,X0) is being_a_retraction by Def9;
hence (Stone-retraction (X,X0)) " F = MaxADSet E by A1, Lm6; :: thesis: verum