let SF be MSSubsetFamily of M; :: thesis: ( SF is properly-lower-bound implies SF is V8() )
assume SF is properly-lower-bound ; :: thesis: SF is V8()
then A1: EmptyMS I in SF ;
let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not SF . i is empty )
assume i in I ; :: thesis: not SF . i is empty
hence not SF . i is empty by A1; :: thesis: verum