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