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