scheme :: CARD_2:sch 3
Sch3{ F1() -> finite set , P1[ object , object ] } :
ex x being set st
( x in F1() & ( for y being set st y in F1() & y <> x holds
not P1[y,x] ) )
provided
A1: F1() <> {} and
A2: for x, y being set st P1[x,y] & P1[y,x] holds
x = y and
A3: for x, y, z being set st P1[x,y] & P1[y,z] holds
P1[x,z]