let H, F be ZF-formula; :: thesis: ( H is atomic implies not F is_immediate_constituent_of H )

A1: now :: thesis: ( H is being_equality & H is atomic implies not F is_immediate_constituent_of H )

assume H is being_equality ; :: thesis: ( H is atomic implies not F is_immediate_constituent_of H )
then H = (Var1 H) '=' (Var2 H) by Th36;
hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th50; :: thesis: verum

end;

A2: now :: thesis: ( H is being_membership & H is atomic implies not F is_immediate_constituent_of H )

assume H is being_membership ; :: thesis: ( H is atomic implies not F is_immediate_constituent_of H )
then H = (Var1 H) 'in' (Var2 H) by Th37;
hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th51; :: thesis: verum

end;

assume H is atomic ; :: thesis: not F is_immediate_constituent_of H
hence not F is_immediate_constituent_of H by A1, A2, Def15; :: thesis: verum