let R be non empty RelStr ; :: thesis: ( the InternalRel of R is symmetric implies f_0 R = f_1 R )

assume the InternalRel of R is symmetric ; :: thesis: f_0 R = f_1 R

hence f_0 R = f_1 R by UncEqTau; :: thesis: verum

assume the InternalRel of R is symmetric ; :: thesis: f_0 R = f_1 R

hence f_0 R = f_1 R by UncEqTau; :: thesis: verum