X /\ Y c= X by XBOOLE_1:17;
hence X /\ Y is loopfull ; :: thesis: verum