let I1, I2 be Subset of V; :: thesis: ( ( for x being set holds
( x in I1 iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) & ( for x being set holds
( x in I2 iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) implies I1 = I2 )
assume that
A1: for x being set holds
( x in I1 iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) and
A2: for x being set holds
( x in I2 iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ; :: thesis: I1 = I2

now :: thesis: for x being set holds
( x in I1 iff x in I2 )

let x be set ; :: thesis: ( x in I1 iff x in I2 )
( x in I1 iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) by A1;
hence ( x in I1 iff x in I2 ) by A2; :: thesis: verum

end;

hence I1 = I2 by TARSKI:1; :: thesis: verum