theorem Th53: :: ZF_LANG:53

for F, G, H being ZF-formula holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )