theorem Th4: :: CLASSES4:4

for X being non empty set holds
( X is axiom_GU4 iff X is FamUnion-closed )