let G, F be Subset-Family of T; :: thesis: ( ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in F ) ) ) implies for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in G ) ) )
assume A6: for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in F ) ) ; :: thesis: for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in G ) )
let A be Subset of T; :: thesis: ( A in G iff ex B being Subset of T st
( A = Int B & B in G ) )
thus ( A in G implies ex B being Subset of T st
( A = Int B & B in G ) ) :: thesis: ( ex B being Subset of T st
( A = Int B & B in G ) implies A in G )
proof
assume A in G ; :: thesis: ex B being Subset of T st
( A = Int B & B in G )
then consider B being Subset of T such that
A7: A = Int B and
A8: B in F by A6;
take C = Int B; :: thesis: ( A = Int C & C in G )
thus A = Int C by A7; :: thesis: C in G
thus C in G by A8, A6; :: thesis: verum
end;
given B being Subset of T such that A9: A = Int B and
A10: B in G ; :: thesis: A in G
consider C being Subset of T such that
A11: B = Int C and
C in F by A10, A6;
A = B by A9, A11;
hence A in G by A10; :: thesis: verum