let r be continuous Function of X,X0; :: thesis:
thus ( r = Stone-retraction (X,X0) implies for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) :: thesis:

assume A1: r = Stone-retraction (X,X0) ; :: thesis:
let M be Subset of X; :: thesis:
reconsider N = M as Subset of X ;
assume A2: M = the carrier of X0 ; :: thesis:
let A be Subset of X; :: thesis:
N is maximal_T_0 by A2, Th11;
then A3: N is T_0 ;
for x being object st x in M /\ (MaxADSet A) holds
x in r .: A

let x be object ; :: thesis:
assume A4: x in M /\ (MaxADSet A) ; :: thesis:
then reconsider c = x as Point of X ;
c in M by A4, XBOOLE_0:def 4;
then A5: M /\ (MaxADSet c) = {c} by A3;
c in MaxADSet A by A4, XBOOLE_0:def 4;
then c in union { (MaxADSet a) where a is Point of X : a in A } by TEX_4:def 11;
then consider D being set such that
A6: c in D and
A7: D in { (MaxADSet a) where a is Point of X : a in A } by TARSKI:def 4;
consider a being Point of X such that
A8: D = MaxADSet a and
A9: a in A by A7;
MaxADSet c = MaxADSet a by A6, A8, TEX_4:21;
then {(r . a)} = {c} by A1, A2, A5, Def10;
hence x in r .: A by A9, FUNCT_2:35, ZFMISC_1:3; :: thesis:

end;

then A10: M /\ (MaxADSet A) c= r .: A by TARSKI:def 3;
for x being object st x in r .: A holds
x in M /\ (MaxADSet A)

let x be object ; :: thesis:
assume A11: x in r .: A ; :: thesis:
then reconsider b = x as Point of X0 ;
consider a being object such that
A12: a in the carrier of X and
A13: a in A and
A14: b = r . a by A11, FUNCT_2:64;
reconsider a = a as Point of X by A12;
{a} c= A by A13, ZFMISC_1:31;
then MaxADSet {a} c= MaxADSet A by TEX_4:31;
then MaxADSet a c= MaxADSet A by TEX_4:28;
then A15: M /\ (MaxADSet a) c= M /\ (MaxADSet A) by XBOOLE_1:26;
M /\ (MaxADSet a) = {b} by A1, A2, A14, Def10;
hence x in M /\ (MaxADSet A) by A15, ZFMISC_1:31; :: thesis:

end;

then r .: A c= M /\ (MaxADSet A) by TARSKI:def 3;
hence M /\ (MaxADSet A) = r .: A by A10, XBOOLE_0:def 10; :: thesis:

end;

assume A16: for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A ; :: thesis:
A17: dom r = [#] X by FUNCT_2:def 1;
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:
assume A18: M = the carrier of X0 ; :: thesis:
let a be Point of X; :: thesis:
M /\ (MaxADSet {a}) = Im (r,a) by A16, A18;
then M /\ (MaxADSet a) = Im (r,a) by TEX_4:28;
hence M /\ (MaxADSet a) = {(r . a)} by A17, FUNCT_1:59; :: thesis:

end;

hence r = Stone-retraction (X,X0) by Def10; :: thesis: