let X be non empty set ; for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds
(low_toler (f,0)) [*] = low_toler (f,0)
let f be PartFunc of [:X,X:],REAL; ( f is nonnegative & f is Reflexive & f is discerning implies (low_toler (f,0)) [*] = low_toler (f,0) )
assume A1:
( f is nonnegative & f is Reflexive & f is discerning )
; (low_toler (f,0)) [*] = low_toler (f,0)
now for p being object st p in (low_toler (f,0)) [*] holds
p in low_toler (f,0)let p be
object ;
( p in (low_toler (f,0)) [*] implies p in low_toler (f,0) )assume A2:
p in (low_toler (f,0)) [*]
;
p in low_toler (f,0)consider x,
y being
object such that A3:
p = [x,y]
by A2, RELAT_1:def 1;
low_toler (
f,
0)
reduces x,
y
by A2, A3, REWRITE1:20;
then consider r being
RedSequence of
low_toler (
f,
0)
such that A4:
(
r . 1
= x &
r . (len r) = y )
by REWRITE1:def 3;
A6:
x is
Element of
X
by A2, A3, ZFMISC_1:87;
0 < len r
by REWRITE1:def 2;
then
0 + 1
<= len r
by NAT_1:13;
then
( 1
in dom r &
len r in dom r )
by FINSEQ_3:25;
then
r . 1
= r . (len r)
by A5, Th2;
hence
p in low_toler (
f,
0)
by A1, A3, A4, A6, Th21;
verum end;
then
( low_toler (f,0) c= (low_toler (f,0)) [*] & (low_toler (f,0)) [*] c= low_toler (f,0) )
by LANG1:18;
hence
(low_toler (f,0)) [*] = low_toler (f,0)
by XBOOLE_0:def 10; verum