let I be set ; :: thesis: for M being ManySortedSet of I
for P being MSSetOp of M st P is reflexive & ( for X being Element of bool M holds P .. X c= X ) holds
P is idempotent
let M be ManySortedSet of I; :: thesis: for P being MSSetOp of M st P is reflexive & ( for X being Element of bool M holds P .. X c= X ) holds
P is idempotent
let P be MSSetOp of M; :: thesis: ( P is reflexive & ( for X being Element of bool M holds P .. X c= X ) implies P is idempotent )
assume that
A1: P is reflexive and
A2: for X being Element of bool M holds P .. X c= X ; :: thesis: P is idempotent
let X be Element of bool M; :: according to CLOSURE1:def 3 :: thesis: P .. X = P .. (P .. X)
A3: P .. X c= P .. (P .. X) by A1;
P .. (P .. X) c= P .. X by A2;
hence P .. X = P .. (P .. X) by A3, PBOOLE:146; :: thesis: verum