let I be set ; :: thesis: for M being ManySortedSet of
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 ; :: 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
hence E c= g . E by Def12; :: according to PBOOLE:def 13 :: thesis: g . E c=' E
thus g . E c=' E by A1, PBOOLE:def 23; :: thesis: verum