P /\ X c= P by XBOOLE_1:17;
hence P /\ X is Relation-like ; :: thesis: verum