NOT O = id (X \ (dom O)) by Th37;
hence NOT O c= id X by SYSREL:15; :: according to MMLQUERY:def 21 :: thesis: verum