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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of A : Class the InternalRel of A,x c= X } or y in the carrier of A )
assume y in { x where x is Element of A : Class the InternalRel of A,x c= X } ; :: thesis: y in the carrier of A
then consider x being Element of A such that
A1: ( y = x & Class the InternalRel of A,x c= X ) ;
thus y in the carrier of A by A1; :: thesis: verum

end;

hence { x where x is Element of A : Class the InternalRel of A,x c= X } is Subset of A ; :: thesis: verum