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 ( card Y in card (bool Y) & card (bool Y) c= card X ) by Th27, Th30;
hence card Y in card X ; :: thesis: not Y,X are_equipotent
then card Y <> card X ;
hence not Y,X are_equipotent by Th21; :: thesis: verum