x 'in' y is Element of WFF by Def8;
hence x 'in' y is ZF-formula-like by Def9; :: thesis: verum