let I be set ; :: thesis: for A being ManySortedSet of holds id (Bool A) is reflexive SetOp of A
let A be ManySortedSet of ; :: 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 12 :: thesis: X c=' f . X
thus X c=' f . X by FUNCT_1:35; :: thesis: verum

end;

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