let T be TopSpace; :: thesis: for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) }
let F be Subset-Family of T; :: thesis: Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } ;
now :: thesis: for C being object st C in { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } holds
C in bool the carrier of T
let C be object ; :: thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } ; :: thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Int B & B in F ) ) ;
hence C in bool the carrier of T ; :: thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } as Subset-Family of T by TARSKI:def 3;
reconsider P = P as Subset-Family of T ;
for X being object holds
( X in Int F iff X in P )
proof
let X be object ; :: thesis: ( X in Int F iff X in P )
A1: now :: thesis: ( X in P implies X in Int F )
assume A2: X in P ; :: thesis: X in Int F
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Int B & B in F ) ) by A2;
hence X in Int F by Def1; :: thesis: verum
end;
now :: thesis: ( X in Int F implies X in P )
assume A3: X in Int F ; :: thesis: X in P
then reconsider C = X as Subset of T ;
ex B being Subset of T st
( C = Int B & B in F ) by A3, Def1;
hence X in P ; :: thesis: verum
end;
hence ( X in Int F iff X in P ) by A1; :: thesis: verum
end;
hence Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } by TARSKI:2; :: thesis: verum