let A, B, X be set ; :: thesis: ( X is Subset of (Funcs (A,B)) implies X is Subset-Family of [:A,B:] )
A1: 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 A1, XBOOLE_1:1; :: thesis: verum