for X, Y being set holds
( [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & card ([:X,{0}:] \/ [:Y,{1}:]) = card ([:Y,{0}:] \/ [:X,{1}:]) ) by Th11;