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_{3}( Element of D) -> Element of Class RD = EqClass (RD,$1);

defpred S_{1}[ 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

_{1}[x,y]
from FILTER_1:sch 2(A2); :: according to LATTICE2:def 1 :: thesis: verum

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

defpred S

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 :: thesis: for x1, x2 being Element of D holds S_{1}[ EqClass (RD,x1), EqClass (RD,x2)]

thus
for x, y being Element of Class RD holds Slet x1, x2 be Element of D; :: thesis: S_{1}[ EqClass (RD,x1), EqClass (RD,x2)]

(F /\/ RD) . (H_{3}(x1),((G /\/ RD) . (H_{3}(x1),H_{3}(x2)))) =
(F /\/ RD) . (H_{3}(x1),H_{3}(G . (x1,x2)))
by Th3

.= H_{3}(F . (x1,(G . (x1,x2))))
by Th3

.= H_{3}(x1)
by A1
;

hence S_{1}[ EqClass (RD,x1), EqClass (RD,x2)]
; :: thesis: verum

end;(F /\/ RD) . (H

.= H

.= H

hence S