reconsider y1 = [the AcceptS of s,(x `1 )] as Element of UnionSt s,t by Th46;
set Sym = the Symbols of s \/ the Symbols of t;
reconsider y2 = x `2 as Element of the Symbols of s \/ the Symbols of t by XBOOLE_0:def 3;
[y1,y2,(x `3 )] in [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:] ;
hence [[the AcceptS of s,(x `1 )],(x `2 ),(x `3 )] is Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:] ; :: thesis: verum