let R be Relation; :: thesis: for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X
let X be set ; :: thesis: ( R is_reflexive_in X implies R ~ is_reflexive_in X )
assume A1: for x being object st x in X holds
[x,x] in R ; :: according to RELAT_2:def 1 :: thesis: R ~ is_reflexive_in X
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R ~ )
assume x in X ; :: thesis: [x,x] in R ~
then [x,x] in R by A1;
hence [x,x] in R ~ by RELAT_1:def 7; :: thesis: verum