theorem Th13: :: BKMODEL4:22

for N1, N2 being Matrix of 3,F_Real st N1 = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> & N2 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> holds
N1 is_reverse_of N2