set SS = AllSymbolsOf S;
set DA = A /\ (((AllSymbolsOf S) *) \ {{}});
set DB = B /\ (((AllSymbolsOf S) *) \ {{}});
reconsider Y = B /\ (((AllSymbolsOf S) *) \ {{}}) as functional set ;
reconsider X = A /\ (((AllSymbolsOf S) *) \ {{}}) as Subset of Y by XBOOLE_1:26;
A1: SymbolsOf X c= SymbolsOf Y by FOMODEL0:46;
let s be Element of S; :: thesis: ( s is A -occurring implies s is B -occurring )
assume s is A -occurring ; :: thesis: s is B -occurring
then s in SymbolsOf X ;
hence s is B -occurring by A1; :: thesis: verum