let x be object ; :: thesis: for X being non empty set

for a1, a2 being non negative Real 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 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; :: 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)

let z1 be object ; :: according to TARSKI:def 3 :: thesis: ( not z1 in Class (R1,x) or 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

for a1, a2 being non negative Real 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 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; :: 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)

let z1 be object ; :: according to TARSKI:def 3 :: thesis: ( not z1 in Class (R1,x) or 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