let X be non empty TopSpace; :: thesis: for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is open holds
A = MaxADSet (M /\ A)
let M be Subset of X; :: thesis: ( M is maximal_T_0 implies for A being Subset of X st A is open holds
A = MaxADSet (M /\ A) )
assume A1: M is maximal_T_0 ; :: thesis: for A being Subset of X st A is open holds
A = MaxADSet (M /\ A)
let A be Subset of X; :: thesis: ( A is open implies A = MaxADSet (M /\ A) )
assume A2: A is open ; :: thesis: A = MaxADSet (M /\ A)
then MaxADSet (M /\ A) = (MaxADSet M) /\ (MaxADSet A) by TEX_4:65;
then A3: MaxADSet (M /\ A) = (MaxADSet M) /\ A by A2, TEX_4:56;
A = the carrier of X /\ A by XBOOLE_1:28;
hence A = MaxADSet (M /\ A) by A1, A3; :: thesis: verum