let TS be TopSpace; :: thesis: 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; :: thesis: Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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)) ; :: thesis: 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 <> {} ;

A14: now :: thesis: ( L /\ Q3 = {} implies (K `) /\ (Q1 /\ Q3) = {} )

assume L /\ Q3 = {} ; :: thesis: (K `) /\ (Q1 /\ Q3) = {}
then Q3 misses (L `) ` ;
then A15: Q3 c= L ` by SUBSET_1:24;
((K `) /\ Q1) /\ ((L `) /\ Q3) = {} /\ Q3 by A9, A13, XBOOLE_1:16;
then ((K `) /\ Q1) /\ Q3 = {} by A15, XBOOLE_1:28;
hence (K `) /\ (Q1 /\ Q3) = {} by XBOOLE_1:16; :: thesis: verum

end;

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; :: thesis: verum