scheme :: CLASSES3:sch 1
ClosedUnderReplacement{ F₁() -> set , F₂() -> Grothendieck of F₁(), F₃( set ) -> set } :

{ F₃(x) where x is Element of F₁() : x in F₁() } in F₂()

provided

A1: for Y being set st Y in F₁() holds
F₃(Y) in F₂()