theorem Th15: :: SUBSTLAT:15

for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )