let Y be set ; :: thesis: for R being Relation of Y st R is_reflexive_in Y holds
Y = field R
let R be Relation of Y; :: thesis: ( R is_reflexive_in Y implies Y = field R )
assume R is_reflexive_in Y ; :: thesis: Y = field R
hence Y c= field R by Th8; :: according to XBOOLE_0:def 10 :: thesis: field R c= Y
field R c= Y \/ Y by RELSET_1:8;
hence field R c= Y ; :: thesis: verum