let R be non empty RelStr ; :: thesis: ( the InternalRel of R is symmetric iff for u, v being Element of R st u in (tau R) . v holds
v in (tau R) . u )

hereby :: thesis: ( ( for u, v being Element of R st u in (tau R) . v holds
v in (tau R) . u ) implies the InternalRel of R is symmetric )

assume A1: the InternalRel of R is symmetric ; :: thesis: for u, v being Element of R st u in (tau R) . v holds
v in (tau R) . u
let u, v be Element of R; :: thesis: ( u in (tau R) . v implies v in (tau R) . u )
assume u in (tau R) . v ; :: thesis: v in (tau R) . u
then u in (UncertaintyMap R) . v by A1, UncEqTau;
then [u,v] in the InternalRel of R by For3;
hence v in (tau R) . u by For3A; :: thesis: verum

end;

assume Z0: for u, v being Element of R st u in (tau R) . v holds
v in (tau R) . u ; :: thesis: the InternalRel of R is symmetric
for a, b being object st [a,b] in the InternalRel of R holds
[b,a] in the InternalRel of R

proof

let a, b be object ; :: thesis: ( [a,b] in the InternalRel of R implies [b,a] in the InternalRel of R )
assume Z1: [a,b] in the InternalRel of R ; :: thesis: [b,a] in the InternalRel of R
then reconsider aa = a, bb = b as Element of R by Lemacik;
bb in (tau R) . aa by Z1, For3A;
then aa in (tau R) . bb by Z0;
hence [b,a] in the InternalRel of R by For3A; :: thesis: verum

end;

hence the InternalRel of R is symmetric by PREFER_1:20; :: thesis: verum