theorem :: FINSET_1:14

for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds
ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] )