let X be non empty set ; :: thesis: for r being Relation of X st r is_reflexive_in X holds
chi (r,[:X,X:]) is reflexive
let r be Relation of X; :: thesis: ( r is_reflexive_in X implies chi (r,[:X,X:]) is reflexive )
assume A1: r is_reflexive_in X ; :: thesis: chi (r,[:X,X:]) is reflexive
for x being Element of X holds (chi (r,[:X,X:])) . (x,x) = 1

proof

let x be Element of X; :: thesis: (chi (r,[:X,X:])) . (x,x) = 1
[x,x] in r by A1, RELAT_2:def 1;
hence (chi (r,[:X,X:])) . (x,x) = 1 by FUNCT_3:def 3; :: thesis: verum

end;

hence chi (r,[:X,X:]) is reflexive ; :: thesis: verum