theorem Th10: :: HEYTING1:10

for A being set
for u being Element of (NormForm A) holds u = FinJoin ((@ u),(Atom A))