proposition: Lemma in_fs_bounded : forall (a : E) (f : E1), Bounded.axioms (in_function_set a f).
proof: Proof. ir. ap Bounded.criterion. apply ex_intro with (powerset (record a f)). ir. ap powerset_inc. ap in_fs_sub_record; au. Qed.
imports: set_theory