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