for x being set st x in P \ X holds
ex y, z being set st x = [y,z] by Def1;
hence P \ X is Relation-like by Def1; :: thesis: verum