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)} ) :: 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 )

proof

assume A1: r = Stone-retraction X,X0 ; :: 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)}
let M be Subset of X; :: thesis: ( M = the carrier of X0 implies for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} )
A2: Stone-retraction X,X0 is being_a_retraction by Def9;
assume M = the carrier of X0 ; :: thesis: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
hence for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} by A1, A2, Lm3; :: thesis: verum

end;

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