:: deftheorem Def13 defines projection WAYBEL_1:def 13 :
for L being non empty RelStr
for p being Function of L,L holds
( p is projection iff ( p is idempotent & p is monotone ) );