consider F being thin_cylinder of A,B;
P2: F in { D where D is Subset of (Funcs B,A) : D is thin_cylinder of A,B } ;

now

let z be set ; :: thesis: ( z in { D where D is Subset of (Funcs B,A) : D is thin_cylinder of A,B } implies z in bool (Funcs B,A) )
assume z in { D where D is Subset of (Funcs B,A) : D is thin_cylinder of A,B } ; :: thesis: z in bool (Funcs B,A)
then ex D being Subset of (Funcs B,A) st
( z = D & D is thin_cylinder of A,B ) ;
hence z in bool (Funcs B,A) ; :: thesis: verum

end;

hence { D where D is Subset of (Funcs B,A) : D is thin_cylinder of A,B } is non empty Subset-Family of (Funcs B,A) by P2, TARSKI:def 3; :: thesis: verum