scheme :: XFAMILY:sch 1
Separation{ F1() -> set , P1[ element ] } :
ex X being set st
for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
proof end;

scheme :: XFAMILY:sch 2
Extensionality{ F1() -> set , F2() -> set , P1[ set ] } :
F1() = F2()
provided
A1: for x being set holds
( x in F1() iff P1[x] ) and
A2: for x being set holds
( x in F2() iff P1[x] )
proof end;

scheme :: XFAMILY:sch 3
SetEq{ P1[ set ] } :
for X1, X2 being set st ( for x being set holds
( x in X1 iff P1[x] ) ) & ( for x being set holds
( x in X2 iff P1[x] ) ) holds
X1 = X2
proof end;