consider D being MSSubsetFamily of A such that
A1: ( D = MSFixPoints C & ClOp->ClSys C = MSClosureStr(# A,D #) ) by Def14;
thus ClOp->ClSys C is strict by A1; :: thesis: verum