let x be set ; :: thesis: for X being non empty set
for a1, a2 being non negative real number st a1 <= a2 holds
for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] holds
Class R1,x c= Class R2,x
let X be non empty set ; :: thesis: for a1, a2 being non negative real number st a1 <= a2 holds
for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] holds
Class R1,x c= Class R2,x
let a1, a2 be non negative real number ; :: thesis: ( a1 <= a2 implies for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] holds
Class R1,x c= Class R2,x )
assume A1: a1 <= a2 ; :: thesis: for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] holds
Class R1,x c= Class R2,x
let f be PartFunc of [:X,X:],REAL ; :: thesis: for R1, R2 being Equivalence_Relation of X st R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] holds
Class R1,x c= Class R2,x
let R1, R2 be Equivalence_Relation of X; :: thesis: ( R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] implies Class R1,x c= Class R2,x )
assume A2: ( R1 = (low_toler f,a1) [*] & R2 = (low_toler f,a2) [*] ) ; :: thesis: Class R1,x c= Class R2,x

now

let z1 be set ; :: thesis: ( z1 in Class R1,x implies z1 in Class R2,x )
assume A3: z1 in Class R1,x ; :: thesis: z1 in Class R2,x
A4: R1 c= R2 by A1, A2, Th10, Th19;
[z1,x] in R1 by A3, EQREL_1:27;
hence z1 in Class R2,x by A4, EQREL_1:27; :: thesis: verum

end;

hence Class R1,x c= Class R2,x by TARSKI:def 3; :: thesis: verum