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

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