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

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