let I be set ; :: thesis: for M being ManySortedSet of
for P, R being MSSetOp of M st P is reflexive & R is reflexive holds
P ** R is reflexive
let M be ManySortedSet of ; :: 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 that
A1: P is reflexive and
A2: R is reflexive ; :: thesis: P ** R is reflexive
let X be Element of bool M; :: according to CLOSURE1:def 2 :: thesis: X c= (P ** R) .. X
A3: doms R = bool M by MSSUBFAM:17;
A4: X c= R .. X by A2, Def2;
R .. X c= P .. (R .. X) by A1, Def2;
then X c= P .. (R .. X) by A4, PBOOLE:15;
hence X c= (P ** R) .. X by A3, Th4, MSSUBFAM:12; :: thesis: verum