EmptyMS I c= M by MBOOLEAN:5;
then EmptyMS I in bool M by MBOOLEAN:1;
then reconsider a = EmptyMS I as Element of bool M by MSSUBFAM:11;
take a ; :: thesis: ( a is V9() & a is V45() )
thus ( a is V9() & a is V45() ) ; :: thesis: verum