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