let F be functional set ; :: thesis: for B being set st B c= F holds
B is functional
let B be set ; :: thesis: ( B c= F implies B is functional )
assume A1: B c= F ; :: thesis: B is functional
let x be set ; :: according to FRAENKEL:def 1 :: thesis: ( x in B implies x is Function )
assume x in B ; :: thesis: x is Function
hence x is Function by A1; :: thesis: verum