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 )
A1:
dom r = [#] X
by FUNCT_2:def 1;
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 A2:
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 A3:
M = the
carrier of
X0
;
:: thesis: for A being Subset of X holds M /\ (MaxADSet A) = r .: A
then
N is
maximal_T_0
by Th11;
then A4:
N is
T_0
by Def4;
let A be
Subset of
X;
:: thesis: M /\ (MaxADSet A) = r .: A
A5:
M /\ (MaxADSet A) c= r .: A
proof
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 A6:
x in M /\ (MaxADSet A)
;
:: thesis: x in r .: A
then reconsider c =
x as
Point of
X ;
c in M
by A6, XBOOLE_0:def 4;
then A7:
M /\ (MaxADSet c) = {c}
by A4, Def2;
c in MaxADSet A
by A6, 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 A8:
c in D
and A9:
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 A10:
D = MaxADSet a
and A11:
a in A
by A9;
MaxADSet c = MaxADSet a
by A8, A10, TEX_4:23;
then
{(r . a)} = {c}
by A2, A3, A7, Def10;
hence
x in r .: A
by A11, FUNCT_2:43, ZFMISC_1:6;
:: thesis: verum
end;
hence
M /\ (MaxADSet A) c= r .: A
by TARSKI:def 3;
:: thesis: verum
end;
r .: A c= M /\ (MaxADSet A)
hence
M /\ (MaxADSet A) = r .: A
by A5, XBOOLE_0:def 10;
:: thesis: verum
end;
assume A17:
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
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)}
hence
r = Stone-retraction X,X0
by Def10; :: thesis: verum