take [[0]] I ; :: thesis: [[0]] I is empty-yielding
let i be set ; :: according to PBOOLE:def 12 :: thesis: ( i in I implies ([[0]] I) . i is empty )
assume i in I ; :: thesis: ([[0]] I) . i is empty
thus ([[0]] I) . i is empty by Th5; :: thesis: verum