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

A2: now

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

end;

now

assume H is being_membership ; :: thesis: not F is_immediate_constituent_of H
then H = (Var1 H) 'in' (Var2 H) by Th54;
hence not F is_immediate_constituent_of H by Th70; :: thesis: verum

end;

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