reconsider D = MSFixPoints C as MSSubsetFamily of A ;
reconsider a = MSClosureStr(# A,D #) as MSClosureSystem of S by Th30;
take a ; :: thesis: ex D being MSSubsetFamily of A st
( D = MSFixPoints C & a = MSClosureStr(# A,D #) )
thus ex D being MSSubsetFamily of A st
( D = MSFixPoints C & a = MSClosureStr(# A,D #) ) ; :: thesis: verum