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 that

A1: R is_reflexive_in X 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

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 that

A1: R is_reflexive_in X 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