set C = id (bool {});
reconsider C = id (bool {}) as Function of (bool {}),(bool {}) ;
take T = 2ndOpStr(# {},C #); :: thesis: T is with_op-open_subsets
T is with_op-open_subsets
proof
{} c= {} ;
then reconsider CC = {} C as Subset of T ;
CC is op-open ;
hence T is with_op-open_subsets ; :: thesis: verum
end;
hence T is with_op-open_subsets ; :: thesis: verum