let I be set ; :: thesis: for M being ManySortedSet of I
for P being MSSetOp of M
for E being Element of bool M st E = M & P is reflexive holds
E = P .. E
let M be ManySortedSet of I; :: thesis: for P being MSSetOp of M
for E being Element of bool M st E = M & P is reflexive holds
E = P .. E
let P be MSSetOp of M; :: thesis: for E being Element of bool M st E = M & P is reflexive holds
E = P .. E
let E be Element of bool M; :: thesis: ( E = M & P is reflexive implies E = P .. E )
assume A1: E = M ; :: thesis: ( not P is reflexive or E = P .. E )
assume P is reflexive ; :: thesis: E = P .. E
hence E c= P .. E by Def2; :: according to PBOOLE:def 10 :: thesis: P .. E c= E
P .. E in bool E by A1, MSSUBFAM:12;
hence P .. E c= E by MBOOLEAN:18; :: thesis: verum