let TS be TopSpace; for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let K, L be Subset of TS; Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let x be object ; TARSKI:def 3 ( not x in Fr K or x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) )
A1:
(L `) /\ (K `) = (K \/ L) `
by XBOOLE_1:53;
assume A2:
x in Fr K
; x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
then reconsider x99 = x as Point of TS ;
A3:
not TS is empty
by A2;
assume A4:
not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
; contradiction
then A5:
not x99 in (Fr (K \/ L)) \/ (Fr (K /\ L))
by XBOOLE_0:def 3;
then
not x99 in Fr (K \/ L)
by XBOOLE_0:def 3;
then consider Q1 being Subset of TS such that
A6:
Q1 is open
and
A7:
x99 in Q1
and
A8:
( K \/ L misses Q1 or (K \/ L) ` misses Q1 )
by A3, Th28;
( (K \/ L) /\ Q1 = {} or ((K \/ L) `) /\ Q1 = {} )
by A8;
then A9:
( (K /\ Q1) \/ (Q1 /\ L) = {} or (L `) /\ ((K `) /\ Q1) = {} )
by A1, XBOOLE_1:16, XBOOLE_1:23;
not x99 in (Fr K) /\ (Fr L)
by A4, XBOOLE_0:def 3;
then
not x99 in Fr L
by A2, XBOOLE_0:def 4;
then consider Q3 being Subset of TS such that
A10:
Q3 is open
and
A11:
x99 in Q3
and
A12:
( L misses Q3 or L ` misses Q3 )
by A3, Th28;
K meets Q1
by A2, A3, A6, A7, Th28;
then A13:
K /\ Q1 <> {}
;
A16:
(L `) \/ (K `) = (K /\ L) `
by XBOOLE_1:54;
not x99 in Fr (K /\ L)
by A5, XBOOLE_0:def 3;
then consider Q2 being Subset of TS such that
A17:
Q2 is open
and
A18:
x99 in Q2
and
A19:
( K /\ L misses Q2 or (K /\ L) ` misses Q2 )
by A3, Th28;
( (K /\ L) /\ Q2 = {} or ((K /\ L) `) /\ Q2 = {} )
by A19;
then A20:
( (K /\ Q2) /\ L = {} or ((K `) /\ Q2) \/ (Q2 /\ (L `)) = {} )
by A16, XBOOLE_1:16, XBOOLE_1:23;
x99 in Q1 /\ Q3
by A7, A11, XBOOLE_0:def 4;
then
K ` meets Q1 /\ Q3
by A2, A3, A6, A10, Th28;
then A21:
Q3 c= L
by A12, A14, SUBSET_1:24;
K ` meets Q2
by A2, A3, A17, A18, Th28;
then
(K `) /\ Q2 <> {}
;
then
(K /\ (Q2 /\ L)) /\ Q3 = {} /\ Q3
by A20, XBOOLE_1:16;
then
K /\ ((Q2 /\ L) /\ Q3) = {}
by XBOOLE_1:16;
then
K /\ (Q2 /\ (L /\ Q3)) = {}
by XBOOLE_1:16;
then
K /\ (Q2 /\ Q3) = {}
by A21, XBOOLE_1:28;
then A22:
K misses Q2 /\ Q3
;
x99 in Q2 /\ Q3
by A18, A11, XBOOLE_0:def 4;
hence
contradiction
by A2, A3, A17, A10, A22, Th28; verum