let I be set ; :: thesis: for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A
let A be ManySortedSet of I; :: thesis: id (Bool A) is reflexive SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
f is reflexive

proof

let X be Element of Bool A; :: according to CLOSURE2:def 10 :: thesis: X c=' f . X
thus X c=' f . X by FUNCT_1:18; :: thesis: verum

end;

hence id (Bool A) is reflexive SetOp of A ; :: thesis: verum