let I be set ; :: thesis: for M being ManySortedSet of I
for P, R being MSSetOp of M st P is reflexive & R is reflexive holds
P ** R is reflexive
let M be ManySortedSet of I; :: thesis: for P, R being MSSetOp of M st P is reflexive & R is reflexive holds
P ** R is reflexive
let P, R be MSSetOp of M; :: thesis: ( P is reflexive & R is reflexive implies P ** R is reflexive )
assume A1: ( P is reflexive & R is reflexive ) ; :: thesis: P ** R is reflexive
let X be Element of bool M; :: according to CLOSURE1:def 1 :: thesis: X c= (P ** R) .. X
( X c= R .. X & R .. X c= P .. (R .. X) ) by A1;
then ( doms R = bool M & X c= P .. (R .. X) ) by MSSUBFAM:17, PBOOLE:13;
hence X c= (P ** R) .. X by Th4, MSSUBFAM:12; :: thesis: verum