set I = { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) } ;
now :: thesis: for x being object st x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) } holds
x in the carrier of V
let x be object ; :: thesis: ( x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) } implies x in the carrier of V )
assume x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) } ; :: thesis: x in the carrier of V
then ex y being Element of V st
( x = y & y in conv A & ( for B being Subset of V holds
( not B c< A or not y in conv B ) ) ) ;
hence x in the carrier of V ; :: thesis: verum
end;
then reconsider I = { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) } as Subset of V by TARSKI:def 3;
take I ; :: thesis: for x being set holds
( x in I iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) )
let x be set ; :: thesis: ( x in I iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) )
hereby :: thesis: ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) implies x in I )
assume x in I ; :: thesis: ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) )
then ex y being Element of V st
( x = y & y in conv A & ( for B being Subset of V holds
( not B c< A or not y in conv B ) ) ) ;
hence ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ; :: thesis: verum
end;
assume ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ; :: thesis: x in I
hence x in I ; :: thesis: verum