deffunc H1( set ) -> set = bool (X . $1);
consider p being FinSequence such that
A1: len p = n and
A2: for i being Nat st i in dom p holds
p . i = H1(i) from FINSEQ_1:sch 2();
 reconsider p = p as n -element FinSequence by A1, CARD_1:def 7;
take p ; :: thesis: for i being Nat st i in Seg n holds
p . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i)
now :: thesis: for i being Nat st i in Seg n holds
p . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i)
let i be Nat; :: thesis: ( i in Seg n implies p . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) )
assume A3: i in Seg n ; :: thesis: p . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i)
reconsider Xi = X . i as set ;
bool Xi c= bool Xi ;
then reconsider BXi = bool Xi as Subset-Family of Xi ;
A4: BXi is cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element Subset-Family of Xi ;
i in dom p by A3, A1, FINSEQ_1:def 3;
hence p . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) by A2, A4; :: thesis: verum
end;
hence for i being Nat st i in Seg n holds
p . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) ; :: thesis: verum