theorem Th13: :: GLIBPRE1:13

for X, x being set st x in X holds
(disjoin (Card (id X))) . x = [:(card x),{x}:]