theorem :: HEYTING2:28

for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))