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
then A1: |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by Th14;
consider x being object such that
A2: x in SF by XBOOLE_0:def 1;
reconsider x = x as Element of Bool M by A2;
x . i in |:SF:| . i by A1, A2;
hence not |:SF:| . i is empty ; :: thesis: verum