:: deftheorem defines =>> HEYTING1:def 7 :
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B =>> C = (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ;