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

A1: now

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

end;

A2: now

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 Th54;
hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th70; :: 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