for x, y being set
for X, Y being finite set
for Fy being finite-yielding Function st x <> y & Fy = (x,y) --> (X,Y) holds
( Card_Intersection (Fy,1) = (card X) + (card Y) & Card_Intersection (Fy,2) = card (X /\ Y) )