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
then A2: E c= P .. E ;
P .. E in bool E by A1, MSSUBFAM:12;
then P .. E c= E by MBOOLEAN:18;
hence E = P .. E by A2, PBOOLE:146; :: thesis: verum