theorem :: EQREL_1:1

for X being set
for R1 being Relation of X holds (nabla X) \/ R1 = nabla X by XBOOLE_1:12;