let F, H be ZF-formula; :: thesis: ( H is atomic implies not F is_immediate_constituent_of H )
A1: ( H is being_equality & H is atomic implies not F is_immediate_constituent_of H ) by Th50;
( H is being_membership & H is atomic implies not F is_immediate_constituent_of H ) by Th51;
hence ( H is atomic implies not F is_immediate_constituent_of H ) by A1; :: thesis: verum