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