reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let r be continuous Function of X,X0; :: thesis: ( r = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} )
thus ( r = Stone-retraction (X,X0) implies for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) by Def9, Lm3; :: thesis: ( ( for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r = Stone-retraction (X,X0) )
assume for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} ; :: thesis: r = Stone-retraction (X,X0)
then for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ;
then r is being_a_retraction by Th20;
hence r = Stone-retraction (X,X0) by Def9; :: thesis: verum