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

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