theorem Th18: :: SUBSTLAT:18

for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B