let TSG1, TSG2 be Subset of (FinTrees the carrier of G); :: thesis: ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG1 ) & ( for o being Symbol of G
for p being FinSequence of TSG1 st o ==> roots p holds
o -tree p in TSG1 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
TSG1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG2 ) & ( for o being Symbol of G
for p being FinSequence of TSG2 st o ==> roots p holds
o -tree p in TSG2 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
TSG2 c= F ) implies TSG1 = TSG2 )
assume A5: ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG1 ) & ( for o being Symbol of G
for p being FinSequence of TSG1 st o ==> roots p holds
o -tree p in TSG1 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
TSG1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG2 ) & ( for o being Symbol of G
for p being FinSequence of TSG2 st o ==> roots p holds
o -tree p in TSG2 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
TSG2 c= F ) & not TSG1 = TSG2 ) ; :: thesis: contradiction
then A6: TSG1 c= TSG2 ;
TSG2 c= TSG1 by A5;
hence contradiction by A5, A6, XBOOLE_0:def 10; :: thesis: verum