theorem Th5: :: HEYTING2:5

for V, C being set
for A, B being Element of SubstitutionSet (V,C) st ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) holds
mi (A ^ B) = A