{ x where x is Element of A : Class ( the InternalRel of A,x) meets X } c= the carrier of A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of A : Class ( the InternalRel of A,x) meets X } or y in the carrier of A )
assume y in { x where x is Element of A : Class ( the InternalRel of A,x) meets X } ; :: thesis: y in the carrier of A
then ex x being Element of A st
( y = x & Class ( the InternalRel of A,x) meets X ) ;
hence y in the carrier of A ; :: thesis: verum

end;

hence { x where x is Element of A : Class ( the InternalRel of A,x) meets X } is Subset of A ; :: thesis: verum