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 z1 in Class (R1,x) ; :: thesis: z1 in Class (R2,x)
then A3: [z1,x] in R1 by EQREL_1:19;
R1 c= R2 by A1, A2, Th10, Th19;
hence z1 in Class (R2,x) by A3, EQREL_1:19; :: thesis: verum

end;

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