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
proof
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;
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 )
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