now :: thesis: for m being Nat st m is_at_least_length_of X^3-2 holds
4 <= m

let m be Nat; :: thesis: ( m is_at_least_length_of X^3-2 implies 4 <= m )
assume B: m is_at_least_length_of X^3-2 ; :: thesis: 4 <= m

now :: thesis: not m < 4

assume m < 4 ; :: thesis: contradiction
then m < 3 + 1 ;
hence contradiction by B, LL0, GAUSSINT:def 14, NAT_1:13; :: thesis: verum

end;

hence 4 <= m ; :: thesis: verum

end;

hence len X^3-2 = 4 by LL0, GAUSSINT:def 14, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: len X^3-1 = 4

now :: thesis: for m being Nat st m is_at_least_length_of X^3-1 holds
4 <= m

let m be Nat; :: thesis: ( m is_at_least_length_of X^3-1 implies 4 <= m )
assume B: m is_at_least_length_of X^3-1 ; :: thesis: 4 <= m

now :: thesis: not m < 4

assume m < 4 ; :: thesis: contradiction
then m < 3 + 1 ;
hence contradiction by B, LL01, GAUSSINT:def 14, NAT_1:13; :: thesis: verum

end;

hence 4 <= m ; :: thesis: verum

end;

hence len X^3-1 = 4 by LL01, GAUSSINT:def 14, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: verum