let A, X be non empty set ; :: thesis: {(chi (A,X))} c= Membership_Funcs X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(chi (A,X))} or x in Membership_Funcs X )
assume x in {(chi (A,X))} ; :: thesis: x in Membership_Funcs X
then x = chi (A,X) by TARSKI:def 1;
hence x in Membership_Funcs X by Def1; :: thesis: verum