let X be non empty set ; :: thesis: for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds
R [*] is Equivalence_Relation of X
let R be Relation of X; :: thesis: ( R is_reflexive_in X & R is_symmetric_in X implies R [*] is Equivalence_Relation of X )
assume A1: ( R is_reflexive_in X & R is_symmetric_in X ) ; :: thesis: R [*] is Equivalence_Relation of X
R [*] is_reflexive_in X by A1, Th5;
then A2: ( dom (R [*] ) = X & field (R [*] ) = X ) by ORDERS_1:98;
A3: R [*] is_symmetric_in X by A1, Th7;
R [*] is_transitive_in X by A1, Th8;
hence R [*] is Equivalence_Relation of X by A2, A3, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum