set S = { f where f is Membership_Func of X : verum } ;

take { f where f is Membership_Func of X : verum } ; :: thesis: for f being object holds

( f in { f where f is Membership_Func of X : verum } iff f is Membership_Func of X )

thus for x being object holds

( x in { f where f is Membership_Func of X : verum } iff x is Membership_Func of X ) :: thesis: verum

take { f where f is Membership_Func of X : verum } ; :: thesis: for f being object holds

( f in { f where f is Membership_Func of X : verum } iff f is Membership_Func of X )

thus for x being object holds

( x in { f where f is Membership_Func of X : verum } iff x is Membership_Func of X ) :: thesis: verum

proof

let x be object ; :: thesis: ( x in { f where f is Membership_Func of X : verum } iff x is Membership_Func of X )

hence x in { f where f is Membership_Func of X : verum } ; :: thesis: verum

end;hereby :: thesis: ( x is Membership_Func of X implies x in { f where f is Membership_Func of X : verum } )

assume
x is Membership_Func of X
; :: thesis: x in { f where f is Membership_Func of X : verum } assume
x in { f where f is Membership_Func of X : verum }
; :: thesis: x is Membership_Func of X

then ex f being Membership_Func of X st x = f ;

hence x is Membership_Func of X ; :: thesis: verum

end;then ex f being Membership_Func of X st x = f ;

hence x is Membership_Func of X ; :: thesis: verum

hence x in { f where f is Membership_Func of X : verum } ; :: thesis: verum