for X, Y being set holds [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y