let H be ZF-formula; :: thesis: ( ( 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)} ) )
thus ( ( 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) ) ) by Lm2; :: thesis: ( ( 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)} ) )
thus ( H is conjunctive implies Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) ) :: thesis: ( H is universal implies Free H = (Free (the_scope_of H)) \ {(bound_in H)} )
proof
assume H is conjunctive ; :: thesis: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H))
hence Free H = union {(Free (the_left_argument_of H)),(Free (the_right_argument_of H))} by Lm2
.= (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by ZFMISC_1:75 ;
:: thesis: verum
end;
assume H is universal ; :: thesis: Free H = (Free (the_scope_of H)) \ {(bound_in H)}
hence Free H = (Free (the_scope_of H)) \ {(bound_in H)} by Lm2; :: thesis: verum