let T be TopSpace; :: thesis: for F, G being Subset-Family of T holds Int (F \/ G) = (Int F) \/ (Int G)
let F, G be Subset-Family of T; :: thesis: Int (F \/ G) = (Int F) \/ (Int G)
for X being object holds
( X in Int (F \/ G) iff X in (Int F) \/ (Int G) )
proof
let X be object ; :: thesis: ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) )
A1: now :: thesis: ( X in (Int F) \/ (Int G) implies X in Int (F \/ G) )
assume A2: X in (Int F) \/ (Int G) ; :: thesis: X in Int (F \/ G)
now :: thesis: X in Int (F \/ G)
per cases ( X in Int F or X in Int G ) by A2, XBOOLE_0:def 3;
suppose A3: X in Int F ; :: thesis: X in Int (F \/ G)
then reconsider X0 = X as Subset of T ;
ex W being Subset of T st
( X0 = Int W & W in F \/ G )
proof
consider Z being Subset of T such that
A4: X0 = Int Z and
A5: Z in F by A3, Def1;
take Z ; :: thesis: ( X0 = Int Z & Z in F \/ G )
thus ( X0 = Int Z & Z in F \/ G ) by A4, A5, XBOOLE_0:def 3; :: thesis: verum
end;
hence X in Int (F \/ G) by Def1; :: thesis: verum
end;
suppose A6: X in Int G ; :: thesis: X in Int (F \/ G)
then reconsider X0 = X as Subset of T ;
ex W being Subset of T st
( X0 = Int W & W in F \/ G )
proof
consider Z being Subset of T such that
A7: X0 = Int Z and
A8: Z in G by A6, Def1;
take Z ; :: thesis: ( X0 = Int Z & Z in F \/ G )
thus ( X0 = Int Z & Z in F \/ G ) by A7, A8, XBOOLE_0:def 3; :: thesis: verum
end;
hence X in Int (F \/ G) by Def1; :: thesis: verum
end;
end;
end;
hence X in Int (F \/ G) ; :: thesis: verum
end;
now :: thesis: ( X in Int (F \/ G) implies X in (Int F) \/ (Int G) )
assume A9: X in Int (F \/ G) ; :: thesis: X in (Int F) \/ (Int G)
then reconsider X0 = X as Subset of T ;
consider W being Subset of T such that
A10: X0 = Int W and
A11: W in F \/ G by A9, Def1;
hence X in (Int F) \/ (Int G) ; :: thesis: verum
end;
hence ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) ) by A1; :: thesis: verum
end;
hence Int (F \/ G) = (Int F) \/ (Int G) by TARSKI:2; :: thesis: verum