take EmptyMS I ; :: thesis: EmptyMS I is V9()
let i be object ; :: according to PBOOLE:def 12 :: thesis: ( i in I implies (EmptyMS I) . i is empty )
assume i in I ; :: thesis: (EmptyMS I) . i is empty
thus (EmptyMS I) . i is empty by Th5; :: thesis: verum