set L = LettersOf S;
set P = OpSymbolsOf S;
let s be Element of S; :: thesis: ( s is literal implies not s is operational )
assume B0: s is literal ; :: thesis: not s is operational
assume s is operational ; :: thesis: contradiction
then ( s in LettersOf S & s in OpSymbolsOf S ) by B0, DefLiteral, DefOperational;
then s in (LettersOf S) /\ (OpSymbolsOf S) by XBOOLE_0:def 4;
hence contradiction by Lm8; :: thesis: verum