theorem Th12: :: SUBSTLAT:12
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B