let TS be TopSpace; :: thesis: for K, L being Subset of TS holds (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let K, L be Subset of TS; :: thesis: (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
A1: Fr L c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by Lm1;
A2: ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) c= (Fr K) \/ (Fr L)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
A3: now :: thesis: ( x in (Fr K) /\ (Fr L) & x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) implies x in (Fr K) \/ (Fr L) )
assume x in (Fr K) /\ (Fr L) ; :: thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
then x in Fr K by XBOOLE_0:def 4;
hence ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) ) by XBOOLE_0:def 3; :: thesis: verum
end;
A4: now :: thesis: ( x in Fr (K \/ L) & x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) implies x in (Fr K) \/ (Fr L) )
assume A5: x in Fr (K \/ L) ; :: thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
Fr (K \/ L) c= (Fr K) \/ (Fr L) by Th33;
hence ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) ) by A5; :: thesis: verum
end;
A6: now :: thesis: ( x in Fr (K /\ L) & x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) implies x in (Fr K) \/ (Fr L) )
assume A7: x in Fr (K /\ L) ; :: thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
Fr (K /\ L) c= (Fr K) \/ (Fr L) by Th32;
hence ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) ) by A7; :: thesis: verum
end;
assume x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) ; :: thesis: x in (Fr K) \/ (Fr L)
then ( x in (Fr (K \/ L)) \/ (Fr (K /\ L)) or x in (Fr K) /\ (Fr L) ) by XBOOLE_0:def 3;
hence x in (Fr K) \/ (Fr L) by A4, A6, A3, XBOOLE_0:def 3; :: thesis: verum
end;
Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by Lm1;
then (Fr K) \/ (Fr L) c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by A1, XBOOLE_1:8;
hence (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by A2; :: thesis: verum