{ x where x is Element of : Class the InternalRel of A,x meets 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 : Class the InternalRel of A,x meets X } or y in the carrier of A )
assume y in { x where x is Element of : Class the InternalRel of A,x meets X } ; :: thesis: y in the carrier of A
then ex x being Element of 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 : Class the InternalRel of A,x meets X } is Subset of ; :: thesis: verum