let X, A, B be set ; :: thesis: ( X is Subset of (Funcs (A,B)) implies X is Subset-Family of [:A,B:] )
B0: Funcs (A,B) c= bool [:A,B:] by FRAENKEL:2;
assume X is Subset of (Funcs (A,B)) ; :: thesis: X is Subset-Family of [:A,B:]
hence X is Subset-Family of [:A,B:] by B0, XBOOLE_1:1; :: thesis: verum