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

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 [*]

hence
R [*] is_reflexive_in X
by RELAT_2:def 1; :: thesis: verum[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;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