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)

{ (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

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
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;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