set FUF = { (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } ;
{ (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } c= bool the carrier of (BoolePoset X)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } or z in bool the carrier of (BoolePoset X) )
assume z in { (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } ; :: thesis: z in bool the carrier of (BoolePoset X)
then ex x being Element of (BoolePoset X) st
( z = uparrow x & ex y being Element of X st x = {y} ) ;
hence z in bool the carrier of (BoolePoset X) ; :: thesis: verum

end;

hence { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } is Subset-Family of (BoolePoset X) ; :: thesis: verum