take M1 = 1,1 --> (0. K); :: thesis: ( M1 is line_circulant & M1 is col_circulant )
thus ( M1 is line_circulant & M1 is col_circulant ) ; :: thesis: verum