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 by Def3; :: thesis: verum