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