let X be non empty TopSpace; :: thesis: for P, Q being Subset of X st ( P is closed or Q is closed ) holds
MaxADSet (P /\ Q) = () /\ ()

let P, Q be Subset of X; :: thesis: ( ( P is closed or Q is closed ) implies MaxADSet (P /\ Q) = () /\ () )
assume A1: ( P is closed or Q is closed ) ; :: thesis: MaxADSet (P /\ Q) = () /\ ()
A2: (MaxADSet P) /\ () c= MaxADSet (P /\ Q)
proof
assume not (MaxADSet P) /\ () c= MaxADSet (P /\ Q) ; :: thesis: contradiction
then consider x being object such that
A3: x in () /\ () and
A4: not x in MaxADSet (P /\ Q) ;
reconsider x = x as Point of X by A3;
now :: thesis: contradiction
per cases ( P is closed or Q is closed ) by A1;
suppose A5: P is closed ; :: thesis: contradiction
then P = MaxADSet P by Th60;
then x in P by ;
then A6: MaxADSet x c= P by ;
A7: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet Q by ;
then consider D being set such that
A8: x in D and
A9: D in { () 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 ;
then b in P /\ Q by ;
then MaxADSet b meets MaxADSet (P /\ Q) by ;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A8, A10; :: thesis: verum
end;
suppose A13: Q is closed ; :: thesis: contradiction
then Q = MaxADSet Q by Th60;
then x in Q by ;
then A14: MaxADSet x c= Q by ;
A15: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet P by ;
then consider D being set such that
A16: x in D and
A17: D in { () 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 ;
then b in P /\ Q by ;
then MaxADSet b meets MaxADSet (P /\ Q) by ;
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= () /\ () by Th37;
hence MaxADSet (P /\ Q) = () /\ () by A2; :: thesis: verum