scheme :: FILTER_1:sch 1
SchAux1{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set ] } :
for x being Element of Class F2() holds P1[x]
provided
A1: for x being Element of F1() holds P1[ EqClass (F2(),x)]