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 )

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

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 Z0:
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;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

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

hence
the InternalRel of R is symmetric
by PREFER_1:20; :: thesis: verum
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;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