reconsider A = 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 a being Point of X holds r . a in MaxADSet a )
thus ( r = Stone-retraction (X,X0) implies for a being Point of X holds r . a in MaxADSet a ) :: thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r = Stone-retraction (X,X0) )
proof
assume A1: r = Stone-retraction (X,X0) ; :: thesis: for a being Point of X holds r . a in MaxADSet a
let a be Point of X; :: thesis: r . a in MaxADSet a
A /\ (MaxADSet a) = {(r . a)} by A1, Def10;
then {(r . a)} c= MaxADSet a by XBOOLE_1:17;
hence r . a in MaxADSet a by ZFMISC_1:31; :: thesis: verum
end;
assume for a being Point of X holds r . a in MaxADSet a ; :: thesis: r = Stone-retraction (X,X0)
then r is being_a_retraction by Th21;
hence r = Stone-retraction (X,X0) by Def9; :: thesis: verum