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 H3( Element of D) -> Element of Class RD = EqClass (RD,$1);
defpred S1[ 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 :: thesis: for x1, x2 being Element of D holds S1[ EqClass (RD,x1), EqClass (RD,x2)]
let x1, x2 be Element of D; :: thesis: S1[ EqClass (RD,x1), EqClass (RD,x2)]
(F /\/ RD) . (H3(x1),((G /\/ RD) . (H3(x1),H3(x2)))) = (F /\/ RD) . (H3(x1),H3(G . (x1,x2))) by Th3
.= H3(F . (x1,(G . (x1,x2)))) by Th3
.= H3(x1) by A1 ;
hence S1[ EqClass (RD,x1), EqClass (RD,x2)] ; :: thesis: verum
end;
thus for x, y being Element of Class RD holds S1[x,y] from FILTER_1:sch 2(A2); :: according to LATTICE2:def 1 :: thesis: verum