ex D being MSSubsetFamily of A st
( D = MSFixPoints C & ClOp->ClSys C = MSClosureStr(# A,D #) ) by Def13;
hence ClOp->ClSys C is strict ; :: thesis: verum