let H, G be Subset-Family of T; :: thesis: ( ( for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Int B & B in F ) ) ) & ( 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 H = G )
assume A1: for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Int B & B in F ) ) ; :: thesis: ( ex A being Subset of T st
( ( A in G implies ex B being Subset of T st
( A = Int B & B in F ) ) implies ( ex B being Subset of T st
( A = Int B & B in F ) & not A in G ) ) or H = G )
assume A2: 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: H = G

now :: thesis: for A being object st A in G holds
A in H

let A be object ; :: thesis: ( A in G implies A in H )
assume A3: A in G ; :: thesis: A in H
then reconsider A0 = A as Subset of T ;
ex B being Subset of T st
( A0 = Int B & B in F ) by A2, A3;
hence A in H by A1; :: thesis: verum

end;

then A4: G c= H ;

now :: thesis: for A being object st A in H holds
A in G

let A be object ; :: thesis: ( A in H implies A in G )
assume A5: A in H ; :: thesis: A in G
then reconsider A0 = A as Subset of T ;
ex B being Subset of T st
( A0 = Int B & B in F ) by A1, A5;
hence A in G by A2; :: thesis: verum

end;

then H c= G ;
hence H = G by A4, XBOOLE_0:def 10; :: thesis: verum