let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a being real number st a >= 0 & f is Reflexive & f is symmetric holds
low_toler f,a is Tolerance of X
let f be PartFunc of [:X,X:],REAL ; :: thesis: for a being real number st a >= 0 & f is Reflexive & f is symmetric holds
low_toler f,a is Tolerance of X
let a be real number ; :: thesis: ( a >= 0 & f is Reflexive & f is symmetric implies low_toler f,a is Tolerance of X )
set T = low_toler f,a;
assume that
A1: a >= 0 and
A2: ( f is Reflexive & f is symmetric ) ; :: thesis: low_toler f,a is Tolerance of X
A3: low_toler f,a is_reflexive_in X by A1, A2, Th16;
A4: dom (low_toler f,a) = X by A1, A2, Th3, Th16;
then A5: field (low_toler f,a) = X \/ (rng (low_toler f,a)) by RELAT_1:def 6
.= X by XBOOLE_1:12 ;
then low_toler f,a is_symmetric_in field (low_toler f,a) by A2, Th17;
hence low_toler f,a is Tolerance of X by A3, A4, A5, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 11; :: thesis: verum