thus
dom (nabla X) c= X
; :: according to XBOOLE_0:def 10,PARTFUN1:def 2 :: thesis: ( X c= dom (nabla X) & nabla X is reflexive )

thus X c= dom (nabla X) :: thesis: nabla X is reflexive

assume x in field (nabla X) ; :: thesis: [x,x] in nabla X

then x in (dom (nabla X)) \/ (rng (nabla X)) ;

hence [x,x] in nabla X by ZFMISC_1:87; :: thesis: verum

thus X c= dom (nabla X) :: thesis: nabla X is reflexive

proof

let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field (nabla X) or [x,x] in nabla X )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom (nabla X) )

assume x in X ; :: thesis: x in dom (nabla X)

then [x,x] in [:X,X:] by ZFMISC_1:87;

hence x in dom (nabla X) by XTUPLE_0:def 12; :: thesis: verum

end;assume x in X ; :: thesis: x in dom (nabla X)

then [x,x] in [:X,X:] by ZFMISC_1:87;

hence x in dom (nabla X) by XTUPLE_0:def 12; :: thesis: verum

assume x in field (nabla X) ; :: thesis: [x,x] in nabla X

then x in (dom (nabla X)) \/ (rng (nabla X)) ;

hence [x,x] in nabla X by ZFMISC_1:87; :: thesis: verum