theorem Th27: :: HEYTING1:27

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