theorem uniolinf: :: PL_AXIOM:16

for X being finite set
for Y being set st Y is c=-linear & X c= union Y & Y <> {} holds
ex Z being set st
( X c= Z & Z in Y )