set F = S -firstChar ;
set L = LettersOf S;
set N = TheNorSymbOf S;
set SS = AllSymbolsOf S;

per cases ( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S ) by Lm23;

suppose w . 1 in LettersOf S ; :: thesis: for b₁ being Element of S st b₁ = (S -firstChar) . w holds
not b₁ is relational

then reconsider IT = (S -firstChar) . w as Element of LettersOf S by FOMODEL0:6;
not IT is relational ;
hence for b₁ being Element of S st b₁ = (S -firstChar) . w holds
not b₁ is relational ; :: thesis: verum

end;

suppose w . 1 = TheNorSymbOf S ; :: thesis: for b₁ being Element of S st b₁ = (S -firstChar) . w holds
not b₁ is relational

hence for b₁ being Element of S st b₁ = (S -firstChar) . w holds
not b₁ is relational by FOMODEL0:6; :: thesis: verum

end;

end;