let I be set ; :: thesis: for M being ManySortedSet of
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
let M be ManySortedSet of ; :: thesis: for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent
let g be SetOp of M; :: thesis: ( g is reflexive & ( for X being Element of Bool M holds g . X c= X ) implies g is idempotent )
assume that
A1: g is reflexive and
A2: for X being Element of Bool M holds g . X c= X ; :: thesis: g is idempotent
let X be Element of Bool M; :: according to CLOSURE2:def 14 :: thesis: g . X = g . (g . X)
thus g . X c= g . (g . X) by A1, Def12; :: according to PBOOLE:def 13 :: thesis: g . (g . X) c=' g . X
thus g . (g . X) c=' g . X by A2; :: thesis: verum