let X be set ; :: thesis: for R being Relation of X st R is_reflexive_in X holds
R [*] is_reflexive_in X
let R be Relation of X; :: thesis: ( R is_reflexive_in X implies R [*] is_reflexive_in X )
assume A1: R is_reflexive_in X ; :: thesis: R [*] is_reflexive_in X
now :: thesis: for x being object st x in X holds
[x,x] in R [*]
let x be object ; :: thesis: ( x in X implies [x,x] in R [*] )
assume x in X ; :: thesis: [x,x] in R [*]
then A2: [x,x] in R by A1, RELAT_2:def 1;
R c= R [*] by LANG1:18;
hence [x,x] in R [*] by A2; :: thesis: verum
end;
hence R [*] is_reflexive_in X by RELAT_2:def 1; :: thesis: verum