let X be non empty TopSpace; :: thesis: for P, Q being Subset of X st ( P is open or Q is open ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
let P, Q be Subset of X; :: thesis: ( ( P is open or Q is open ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) )
assume A1: ( P is open or Q is open ) ; :: thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
A2: MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q) by Th39;
(MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q)

proof

assume not (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) ; :: thesis: contradiction
then consider x being set such that
A3: x in (MaxADSet P) /\ (MaxADSet Q) and
A4: not x in MaxADSet (P /\ Q) by TARSKI:def 3;
reconsider x = x as Point of X by A3;

now

per cases ( P is open or Q is open ) by A1;

suppose A5: P is open ; :: thesis: contradiction

then P = MaxADSet P by Th58;
then x in P by A3, XBOOLE_0:def 4;
then A6: MaxADSet x c= P by A5, Th26;
x in MaxADSet Q by A3, XBOOLE_0:def 4;
then consider D being set such that
A7: x in D and
A8: D in { (MaxADSet b) where b is Point of X : b in Q } by TARSKI:def 4;
consider b being Point of X such that
A9: D = MaxADSet b and
A10: b in Q by A8;
A11: MaxADSet x = MaxADSet b by A7, A9, Th23;
{b} c= MaxADSet b by Th14;
then A12: b in MaxADSet b by ZFMISC_1:37;
then A13: b in P /\ Q by A6, A10, A11, XBOOLE_0:def 4;
P /\ Q c= MaxADSet (P /\ Q) by Th34;
then MaxADSet b meets MaxADSet (P /\ Q) by A12, A13, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th32;
hence contradiction by A4, A7, A9; :: thesis: verum

end;

suppose A14: Q is open ; :: thesis: contradiction

then Q = MaxADSet Q by Th58;
then x in Q by A3, XBOOLE_0:def 4;
then A15: MaxADSet x c= Q by A14, Th26;
x in MaxADSet P by A3, XBOOLE_0:def 4;
then consider D being set such that
A16: x in D and
A17: D in { (MaxADSet b) where b is Point of X : b in P } by TARSKI:def 4;
consider b being Point of X such that
A18: D = MaxADSet b and
A19: b in P by A17;
A20: MaxADSet x = MaxADSet b by A16, A18, Th23;
{b} c= MaxADSet b by Th14;
then A21: b in MaxADSet b by ZFMISC_1:37;
then A22: b in P /\ Q by A15, A19, A20, XBOOLE_0:def 4;
P /\ Q c= MaxADSet (P /\ Q) by Th34;
then MaxADSet b meets MaxADSet (P /\ Q) by A21, A22, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th32;
hence contradiction by A4, A16, A18; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) by A2, XBOOLE_0:def 10; :: thesis: verum