ex T being Subset-Family of (S *) st
for A being Subset of (S *) holds
( A in T iff S₁[A] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of (S *) st
for A being Subset of (S *) holds
( A in b₁ iff ex s being FinSequence of S st A = Finseq-EQclass s ) ; :: thesis: verum