let X be surreal-membered set ; :: thesis: card X = card (-- X)
-- (-- X) = X by Th15;
then ( card (-- X) c= card X & card X c= card (-- X) ) by Th16;
hence card X = card (-- X) by XBOOLE_0:def 10; :: thesis: verum