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;

now :: thesis: X0 in (Int F) \/ (Int G)

per cases ( W in F or W in G ) by A11, XBOOLE_0:def 3;

suppose W in F ; :: thesis: X0 in (Int F) \/ (Int G)

then X0 in Int F by A10, Def1;
hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose W in G ; :: thesis: X0 in (Int F) \/ (Int G)

then X0 in Int G by A10, Def1;
hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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