let I1, I2 be Subset-Family of Omega; :: thesis: ( ( for A being Subset of Omega holds
( A in I1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in I2 iff A /\ X in G ) ) implies I1 = I2 )
assume A2: for A being Subset of Omega holds
( A in I1 iff A /\ X in G ) ; :: thesis: ( ex A being Subset of Omega st
( ( A in I2 implies A /\ X in G ) implies ( A /\ X in G & not A in I2 ) ) or I1 = I2 )
assume A3: for A being Subset of Omega holds
( A in I2 iff A /\ X in G ) ; :: thesis: I1 = I2
now :: thesis: for A being Subset of Omega holds
( A in I1 iff A in I2 )
let A be Subset of Omega; :: thesis: ( A in I1 iff A in I2 )
( A in I1 iff A /\ X in G ) by A2;
hence ( A in I1 iff A in I2 ) by A3; :: thesis: verum
end;
hence I1 = I2 by SUBSET_1:3; :: thesis: verum