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

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