scheme :: FRAENKEL:sch 23
Finiteness{ F1() -> non empty set , F2() -> Element of Fin F1(), P1[ Element of F1(), Element of F1()] } :
for x being Element of F1() st x in F2() holds
ex y being Element of F1() st
( y in F2() & P1[y,x] & ( for z being Element of F1() st z in F2() & P1[z,y] holds
P1[y,z] ) )
provided
A1: for x being Element of F1() holds P1[x,x] and
A2: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds
P1[x,z]