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