let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a being Real 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 st a >= 0 & f is Reflexive & f is symmetric holds
low_toler (f,a) is Tolerance of X
let a be Real; :: 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 2, RELAT_2:def 9, RELAT_2:def 11; :: thesis: verum