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

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