let D be non empty set ; :: thesis: for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F absorbs G holds
F /\/ RD absorbs G /\/ RD
let RD be Equivalence_Relation of D; :: thesis: for F, G being BinOp of D,RD st F absorbs G holds
F /\/ RD absorbs G /\/ RD
let F, G be BinOp of D,RD; :: thesis: ( F absorbs G implies F /\/ RD absorbs G /\/ RD )
deffunc H₃( Element of D) -> Element of Class RD = EqClass RD,$1;
defpred S₁[ Element of Class RD, Element of Class RD] means (F /\/ RD) . $1,((G /\/ RD) . $1,$2) = $1;
assume A1: for x, y being Element of D holds F . x,(G . x,y) = x ; :: according to LATTICE2:def 1 :: thesis: F /\/ RD absorbs G /\/ RD

A2: now

let x1, x2 be Element of D; :: thesis: S₁[ EqClass RD,x1, EqClass RD,x2]
(F /\/ RD) . H₃(x1),((G /\/ RD) . H₃(x1),H₃(x2)) = (F /\/ RD) . H₃(x1),H₃(G . x1,x2) by Th3
.= H₃(F . x1,(G . x1,x2)) by Th3
.= H₃(x1) by A1 ;
hence S₁[ EqClass RD,x1, EqClass RD,x2] ; :: thesis: verum

end;

thus for x, y being Element of Class RD holds S₁[x,y] from FILTER_1:sch 2(A2); :: according to LATTICE2:def 1 :: thesis: verum