theorem Th12: :: HEYTING3:12

for V, C being set
for a, b being Element of (SubstPoset (V,C)) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )