scheme :: ABCMIZ_A:sch 1
MinimalElement{ F1() -> non empty finite set , P1[ set , set ] } :
ex x being set st
( x in F1() & ( for y being set st y in F1() holds
not P1[y,x] ) )
provided
A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
not P1[y,x] and
A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds
P1[x,z]