theorem Th4: :: HEYTING2:4

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