let I be set ; :: thesis: for A being ManySortedSet of I holds id (bool A) is reflexive MSSetOp of A
let A be ManySortedSet of I; :: thesis: id (bool A) is reflexive MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
a is reflexive

proof

let b be Element of bool A; :: according to CLOSURE1:def 1 :: thesis: b c= a .. b
thus b c= a .. b by Th8; :: thesis: verum

end;

hence id (bool A) is reflexive MSSetOp of A ; :: thesis: verum