let I1, I2 be Subset of V; ( ( 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 ) ) ) )
; I1 = I2
hence
I1 = I2
by TARSKI:2; verum