(* Title: Examples/SML_Relativization/Foundations/Set_Ext.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section‹Extension of the theory \<^text>‹Set›› theory Set_Ext imports Main begin lemma set_comp_pair: "{f t r |t r. P t r} = {x. ∃t r. P t r ∧ x = (f t r)}" by auto lemma image_iff': "(∀x∈A. f x ∈ B) = (f ` A ⊆ B)" by auto text‹\newpage› end