( |[1,0]| `1 = 1 & |[1,0]| `2 = 0 & |[0,1]| `1 = 0 & |[0,1]| `2 = 1 & |[0,0]| `1 = 0 & |[0,0]| `2 = 0 ) by EUCLID:52;
hence ( |[1,0]| <> |[0,1]| & |[1,0]| <> |[0,0]| & |[0,1]| <> |[0,0]| ) ; :: thesis: verum