let X be set ; :: thesis: for B being SetSequence of X

for n being Nat holds { (B . k) where k is Nat : n <= k } is Subset-Family of X

let B be SetSequence of X; :: thesis: for n being Nat holds { (B . k) where k is Nat : n <= k } is Subset-Family of X

let n be Nat; :: thesis: { (B . k) where k is Nat : n <= k } is Subset-Family of X

set Y1 = { (B . k) where k is Nat : n <= k } ;

{ (B . k) where k is Nat : n <= k } c= bool X

for n being Nat holds { (B . k) where k is Nat : n <= k } is Subset-Family of X

let B be SetSequence of X; :: thesis: for n being Nat holds { (B . k) where k is Nat : n <= k } is Subset-Family of X

let n be Nat; :: thesis: { (B . k) where k is Nat : n <= k } is Subset-Family of X

set Y1 = { (B . k) where k is Nat : n <= k } ;

{ (B . k) where k is Nat : n <= k } c= bool X

proof

hence
{ (B . k) where k is Nat : n <= k } is Subset-Family of X
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (B . k) where k is Nat : n <= k } or x in bool X )

assume x in { (B . k) where k is Nat : n <= k } ; :: thesis: x in bool X

then consider k being Nat such that

A1: ( x = B . k & n <= k ) ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

x = B . k by A1;

hence x in bool X ; :: thesis: verum

end;assume x in { (B . k) where k is Nat : n <= k } ; :: thesis: x in bool X

then consider k being Nat such that

A1: ( x = B . k & n <= k ) ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

x = B . k by A1;

hence x in bool X ; :: thesis: verum