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

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