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 () . v by ;
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 ;
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