let R be non empty RelStr ; :: thesis: ( the InternalRel of R is symmetric implies UncertaintyMap R = tau R )
assume AA: the InternalRel of R is symmetric ; :: thesis: UncertaintyMap R = tau R
set f = UncertaintyMap R;
set g = tau R;
for x being Element of R holds (UncertaintyMap R) . x = (tau R) . x

proof

let x be Element of R; :: thesis: (UncertaintyMap R) . x = (tau R) . x
Z2: (UncertaintyMap R) . x = Coim ( the InternalRel of R,x) by DefUnc;
ZZ: Im ( the InternalRel of R,x) c= Coim ( the InternalRel of R,x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Im ( the InternalRel of R,x) or y in Coim ( the InternalRel of R,x) )
assume y in Im ( the InternalRel of R,x) ; :: thesis: y in Coim ( the InternalRel of R,x)
then [x,y] in the InternalRel of R by RELAT_1:169;
then B2: [y,x] in the InternalRel of R by AA, PREFER_1:20;
x in {x} by TARSKI:def 1;
hence y in Coim ( the InternalRel of R,x) by B2, RELAT_1:def 14; :: thesis: verum

end;

Coim ( the InternalRel of R,x) c= Im ( the InternalRel of R,x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Coim ( the InternalRel of R,x) or y in Im ( the InternalRel of R,x) )
assume y in Coim ( the InternalRel of R,x) ; :: thesis: y in Im ( the InternalRel of R,x)
then consider yy being object such that
B2: ( [y,yy] in the InternalRel of R & yy in {x} ) by RELAT_1:def 14;
yy = x by TARSKI:def 1, B2;
then [x,y] in the InternalRel of R by B2, PREFER_1:20, AA;
hence y in Im ( the InternalRel of R,x) by RELAT_1:169; :: thesis: verum

end;

hence (UncertaintyMap R) . x = (tau R) . x by ZZ, DefTau, Z2; :: thesis: verum

end;

hence UncertaintyMap R = tau R ; :: thesis: verum