let Y, X be set ; :: thesis: ( bool Y c= X implies ( card Y in card X & not Y,X are_equipotent ) )
assume bool Y c= X ; :: thesis: ( card Y in card X & not Y,X are_equipotent )
then A1: card (bool Y) c= card X by Th27;
card Y in card (bool Y) by Th30;
hence card Y in card X by A1; :: thesis: not Y,X are_equipotent
then card Y <> card X ;
hence not Y,X are_equipotent by Th21; :: thesis: verum