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 A1: ( a >= 0 & f is Reflexive & f is symmetric ) ; :: thesis: low_toler f,a is Tolerance of X
then A2: low_toler f,a is_reflexive_in X by Th16;
A3: dom (low_toler f,a) = X by A1, Th3, Th16;
then A4: 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 A1, Th17;
hence low_toler f,a is Tolerance of X by A2, A3, A4, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 11; :: thesis: verum