let I be set ; :: thesis: for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let M be ManySortedSet of I; :: thesis: for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let g, h be SetOp of M; :: thesis: ( g is reflexive & h is reflexive implies g * h is reflexive )
assume A1: ( g is reflexive & h is reflexive ) ; :: thesis: g * h is reflexive
let X be Element of Bool M; :: according to CLOSURE2:def 10 :: thesis: X c=' (g * h) . X
( X c= h . X & h . X c= g . (h . X) ) by A1;
then ( dom h = Bool M & X c= g . (h . X) ) by FUNCT_2:def 1, PBOOLE:13;
hence X c=' (g * h) . X by FUNCT_1:13; :: thesis: verum