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

let P, Q be Subset of X; :: thesis: ( ( P is closed or Q is closed ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) )

assume A1: ( P is closed or Q is closed ) ; :: thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

A2: (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q)

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

MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

let P, Q be Subset of X; :: thesis: ( ( P is closed or Q is closed ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) )

assume A1: ( P is closed or Q is closed ) ; :: thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

A2: (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q)

proof

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

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( P is closed or Q is closed )
by A1;

end;

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

then
P = MaxADSet P
by Th60;

then x in P by A3, XBOOLE_0:def 4;

then A6: MaxADSet x c= P by A5, Th23;

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;then x in P by A3, XBOOLE_0:def 4;

then A6: MaxADSet x c= P by A5, Th23;

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

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

then
Q = MaxADSet Q
by Th60;

then x in Q by A3, XBOOLE_0:def 4;

then A14: MaxADSet x c= Q by A13, Th23;

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;then x in Q by A3, XBOOLE_0:def 4;

then A14: MaxADSet x c= Q by A13, Th23;

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

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