let I be set ; :: thesis: for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let M be ManySortedSet of I; :: thesis: for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let E be Element of Bool M; :: thesis: for g being SetOp of M st E = M & g is reflexive holds
E = g . E
let g be SetOp of M; :: thesis: ( E = M & g is reflexive implies E = g . E )
assume A1: E = M ; :: thesis: ( not g is reflexive or E = g . E )
assume g is reflexive ; :: thesis: E = g . E
then A2: E c= g . E ;
g . E c= E by A1, PBOOLE:def 18;
hence E = g . E by A2, PBOOLE:146; :: thesis: verum