let I be set ; :: thesis: for M being ManySortedSet of I
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 I; :: 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 12 :: thesis: g . X = g . (g . X)
A3: g . X c= g . (g . X) by A1;
g . (g . X) c= g . X by A2;
hence g . X = g . (g . X) by A3, PBOOLE:146; :: thesis: verum