set F = the thin_cylinder of A,B;

A1: now :: thesis: for z being object st z in { D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } holds
z in bool (Funcs (B,A))

let z be object ; :: 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;

the thin_cylinder of A,B in { D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } ;
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 A1, TARSKI:def 3; :: thesis: verum