theorem Th2: :: HENMODEL:2

for A being non empty finite Subset of NAT holds
( union A in A & ( for a being set holds
( not a in A or a in union A or a = union A ) ) )