let X, Y be set ; :: thesis: ( succ X c= Y implies X c= Y )
X c= succ X by XBOOLE_1:7;
hence ( succ X c= Y implies X c= Y ) ; :: thesis: verum