:: deftheorem defines nabla EQREL_1:def 1 :
for X being set holds nabla X = [:X,X:];