theorem Th23: :: SUBSTLAT:23

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