:: deftheorem defines SubstPoset HEYTING3:def 1 :
for V, C being set holds SubstPoset (V,C) = LattPOSet (SubstLatt (V,C));