theorem :: ZF_MODEL:1

for H being ZF-formula holds
( ( H is being_equality implies Free H = {(Var1 H),(Var2 H)} ) & ( H is being_membership implies Free H = {(Var1 H),(Var2 H)} ) & ( H is negative implies Free H = Free (the_argument_of H) ) & ( H is conjunctive implies Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) ) & ( H is universal implies Free H = (Free (the_scope_of H)) \ {(bound_in H)} ) )