set C = id (bool {});
reconsider C = id (bool {}) as Function of (bool {}),(bool {}) ;
take T = 1stOpStr(# {},C #); :: thesis: T is with_op-closed_subsets
T is with_op-closed_subsets

proof

{} c= {} ;
then reconsider CC = {} C as Subset of T ;
CC is op-closed ;
hence T is with_op-closed_subsets ; :: thesis: verum

end;

hence T is with_op-closed_subsets ; :: thesis: verum