let X be non empty TopSpace; 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; ( ( P is open or Q is open ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) )
assume A1:
( P is open or Q is open )
; 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)
;
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 contradictionper cases
( P is open or Q is open )
by A1;
suppose A5:
P is
open
;
contradictionthen
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;
verum end; suppose A13:
Q is
open
;
contradictionthen
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;
verum end;
hence
contradiction
;
verum
end;
MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q)
by Th37;
hence
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
by A2; verum