let X, Y be set ; :: thesis: (id (X \ Y)) \ (id X) = {}
id (X \ Y) c= id X by Th33;
hence (id (X \ Y)) \ (id X) = {} by XBOOLE_1:37; :: thesis: verum