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
proof
let x be object ; :: thesis: ( x in { f where f is Membership_Func of X : verum } iff x is Membership_Func of X )
hereby :: thesis: ( x is Membership_Func of X implies 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;
assume x is Membership_Func of X ; :: thesis: x in { f where f is Membership_Func of X : verum }
hence x in { f where f is Membership_Func of X : verum } ; :: thesis: verum
end;