let X, Y be set ; :: thesis: ( <:{},X,Y:> is total implies X = {} )
dom {} = {} ;
hence ( <:{},X,Y:> is total implies X = {} ) by Th40, XBOOLE_1:3; :: thesis: verum