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

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

hence
UncertaintyMap R = tau R
; :: thesis: verum
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)

end;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

Coim ( the InternalRel of R,x) c= Im ( the InternalRel of R,x)
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;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

proof

hence
(UncertaintyMap R) . x = (tau R) . x
by ZZ, DefTau, Z2; :: thesis: verum
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;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