take 3 ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not 3 <= b₁ or <%c,b,a%> . b₁ = 0. L )
let n be Nat; :: thesis: ( not 3 <= n or <%c,b,a%> . n = 0. L )
thus ( not 3 <= n or <%c,b,a%> . n = 0. L ) by qua1; :: thesis: verum