[*0,1*] = [*0,1,0,0*] by Lm4;
hence ( Rea <i> = 0 & Im1 <i> = 1 & Im2 <i> = 0 & Im3 <i> = 0 ) by Lm3, Th23; :: thesis: verum