take 3 ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not 3 <= b₁ or <%z0,z1,z2%> . b₁ = 0. L )
thus for b₁ being set holds
( not 3 <= b₁ or <%z0,z1,z2%> . b₁ = 0. L ) by Th24; :: thesis: verum