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
proof
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;
hence { (B . k) where k is Nat : n <= k } is Subset-Family of X ; :: thesis: verum