set X = { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ;

( a,b // K & b in P ) } is Subset of AS by TARSKI:def 3; :: thesis: verum

( a,b // K & b in P ) } ;

now :: thesis: for x being object st x in { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } holds

x in the carrier of AS

hence
{ a where a is Element of AS : ex b being Element of AS st ( a,b // K & b in P ) } holds

x in the carrier of AS

let x be object ; :: thesis: ( x in { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } implies x in the carrier of AS )

assume x in { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ; :: thesis: x in the carrier of AS

then ex a being Element of AS st

( a = x & ex b being Element of AS st

( a,b // K & b in P ) ) ;

hence x in the carrier of AS ; :: thesis: verum

end;( a,b // K & b in P ) } implies x in the carrier of AS )

assume x in { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ; :: thesis: x in the carrier of AS

then ex a being Element of AS st

( a = x & ex b being Element of AS st

( a,b // K & b in P ) ) ;

hence x in the carrier of AS ; :: thesis: verum

( a,b // K & b in P ) } is Subset of AS by TARSKI:def 3; :: thesis: verum