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