for P being set
for F being FinSequence st P is cup-closed & {} in P & ( for n being Nat st n in dom F holds
F . n in P ) holds
Union F in P