let I1, I2 be Subset-Family of Omega; ( ( 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 )
; ( 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 )
; I1 = I2
now for A being Subset of Omega holds
( A in I1 iff A in I2 )let A be
Subset of
Omega;
( 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;
verum end;
hence
I1 = I2
by SUBSET_1:3; verum