let X be set ; :: thesis: for B being Subset-Family of X st {} in B holds
<.B.] = bool X
let B be Subset-Family of X; :: thesis: ( {} in B implies <.B.] = bool X )
assume A1: {} in B ; :: thesis: <.B.] = bool X
thus <.B.] c= bool X ; :: according to XBOOLE_0:def 10 :: thesis: bool X c= <.B.]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in <.B.] )
assume x in bool X ; :: thesis: x in <.B.]
then reconsider x0 = x as Subset of X ;
( {} is Element of B & {} c= x0 ) by A1;
hence x in <.B.] by def3; :: thesis: verum