theorem Th20: :: HEYTING1:20

for A being set
for a being Element of DISJOINT_PAIRS A
for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= c \/ a ) ) holds
ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a )