let X be non empty set ; :: thesis: for R being Relation of X st R is_reflexive_in X holds
( R is reflexive & field R = X )
let R be Relation of X; :: thesis: ( R is_reflexive_in X implies ( R is reflexive & field R = X ) )
assume A1: R is_reflexive_in X ; :: thesis: ( R is reflexive & field R = X )
then X = field R by Th9;
hence ( R is reflexive & field R = X ) by A1, RELAT_2:def 9; :: thesis: verum