theorem Th21: :: POLYFORM:23

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