let X be set ; :: thesis: for B being SetSequence of X
for n being Element of NAT holds { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X
let B be SetSequence of X; :: thesis: for n being Element of NAT holds { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X
let n be Element of NAT ; :: thesis: { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X
set Y1 = { (B . k) where k is Element of NAT : n <= k } ;
{ (B . k) where k is Element of NAT : n <= k } c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (B . k) where k is Element of NAT : n <= k } or x in bool X )
assume x in { (B . k) where k is Element of NAT : n <= k } ; :: thesis: x in bool X
then ex k being Element of NAT st
( x = B . k & n <= k ) ;
hence x in bool X ; :: thesis: verum

end;

hence { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X ; :: thesis: verum