let SF be MSSubsetFamily of M; :: thesis: ( SF is properly-lower-bound implies SF is non-empty )
assume SF is properly-lower-bound ; :: thesis: SF is non-empty
then A1: [[0]] I in SF by Def8;
let i be set ; :: according to PBOOLE:def 16 :: 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, PBOOLE:def 4; :: thesis: verum