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

( 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 object holds

( x in I1 iff x in I2 )

hence
I1 = I2
by TARSKI:2; :: thesis: verum( x in I1 iff x in I2 )

let x be object ; :: 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;( 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