scheme :: LMOD_7:sch 10
Fr4{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> set , F₄() -> Element of F₁(), F₅( object ) -> set , P₁[ object , object ], P₂[ object , object ] } :

( F₄() in F₅(F₃()) iff for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] )

provided

A1: F₅(F₃()) = { a where a is Element of F₁() : P₂[a,F₃()] } and
A2: ( P₂[F₄(),F₃()] iff for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] )