:: deftheorem Def6 defines pi CARD_3:def 6 :
for x being object
for X, b₃ being set holds
( b₃ = pi (X,x) iff for y being object holds
( y in b₃ iff ex f being Function st
( f in X & y = f . x ) ) );