let R be Relation; :: thesis: for Y being set st R is_reflexive_in Y holds

Y c= field R

let Y be set ; :: thesis: ( R is_reflexive_in Y implies Y c= field R )

assume A1: R is_reflexive_in Y ; :: thesis: Y c= field R

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in field R )

assume x in Y ; :: thesis: x in field R

then [x,x] in R by A1;

hence x in field R by RELAT_1:15; :: thesis: verum

Y c= field R

let Y be set ; :: thesis: ( R is_reflexive_in Y implies Y c= field R )

assume A1: R is_reflexive_in Y ; :: thesis: Y c= field R

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in field R )

assume x in Y ; :: thesis: x in field R

then [x,x] in R by A1;

hence x in field R by RELAT_1:15; :: thesis: verum