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) /\ (MaxADSet Q) c= MaxADSet (P /\ Q)

proof

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

now :: thesis: contradiction

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

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

then P = MaxADSet P by Th56;
then x in P by A3, XBOOLE_0:def 4;
then A6: MaxADSet x c= P by A5, Th24;
A7: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet Q by A3, XBOOLE_0:def 4;
then consider D being set such that
A8: x in D and
A9: 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
A10: D = MaxADSet b and
A11: b in Q by A9;
{b} c= MaxADSet b by Th12;
then A12: b in MaxADSet b by ZFMISC_1:31;
MaxADSet x = MaxADSet b by A8, A10, Th21;
then b in P /\ Q by A6, A11, A12, XBOOLE_0:def 4;
then MaxADSet b meets MaxADSet (P /\ Q) by A12, A7, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A8, A10; :: thesis: verum

end;

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

then Q = MaxADSet Q by Th56;
then x in Q by A3, XBOOLE_0:def 4;
then A14: MaxADSet x c= Q by A13, Th24;
A15: P /\ Q c= MaxADSet (P /\ Q) by Th32;
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;
{b} c= MaxADSet b by Th12;
then A20: b in MaxADSet b by ZFMISC_1:31;
MaxADSet x = MaxADSet b by A16, A18, Th21;
then b in P /\ Q by A14, A19, A20, XBOOLE_0:def 4;
then MaxADSet b meets MaxADSet (P /\ Q) by A20, A15, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A16, A18; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q) by Th37;
hence MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) by A2; :: thesis: verum