then reconsider Y1 = { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ; defpred S1[ set ] means ( $1 in B2 & $1 c= z1 ); reconsider Y = Y as Subset-Family of T1 ; reconsider Y1 = Y1 as Subset-Family of T1 ; reconsider Y3 = Y1 as Subset-Family of T2 byA1; A6:
Y c= upV