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 Subset 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 Subset 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 Subset 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 Subset of X holds M /\ (MaxADSet A) = r .: A
let M be Subset of X; :: thesis: ( M = the carrier of X0 implies for A being Subset of X holds M /\ (MaxADSet A) = r .: A )
reconsider N = M as Subset of X ;
assume A2: M = the carrier of X0 ; :: thesis: for A being Subset of X holds M /\ (MaxADSet A) = r .: A
let A be Subset of X; :: thesis: M /\ (MaxADSet A) = r .: A
N is maximal_T_0 by A2, Th11;
then A3: N is T_0 by Def4;
for x being set st x in M /\ (MaxADSet A) holds
x in r .: A

proof

let x be set ; :: thesis: ( x in M /\ (MaxADSet A) implies x in r .: A )
assume A4: x in M /\ (MaxADSet A) ; :: thesis: x in r .: A
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, Def2;
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: verum

end;

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

proof

let x be set ; :: thesis: ( x in r .: A implies x in M /\ (MaxADSet A) )
assume A11: x in r .: A ; :: thesis: x in M /\ (MaxADSet A)
then reconsider b = x as Point of X0 ;
consider a being set 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: verum

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: verum

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: r = Stone-retraction (X,X0)
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)}

proof

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)} )
assume A18: M = the carrier of X0 ; :: thesis: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
let a be Point of X; :: thesis: M /\ (MaxADSet a) = {(r . a)}
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: verum

end;

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