let X, Y 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 (bool Y) c= card X by Th10;
hence card Y in card X by Th13; :: thesis: not Y,X are_equipotent
then card Y <> card X ;
hence not Y,X are_equipotent by Th4; :: thesis: verum