let G be non empty DTConstrStr ; :: thesis: for t being set holds
( not t in TS G or ex d being Symbol of G st
( d in Terminals G & t = root-tree d ) or ex o being Symbol of G ex p being FinSequence of TS G st
( o ==> roots p & t = o -tree p ) )
let t be set ; :: thesis: ( not t in TS G or ex d being Symbol of G st
( d in Terminals G & t = root-tree d ) or ex o being Symbol of G ex p being FinSequence of TS G st
( o ==> roots p & t = o -tree p ) )
assume that
A1: t in TS G and
A2: for d being Symbol of G holds
( not d in Terminals G or not t = root-tree d ) and
A3: for o being Symbol of G
for p being FinSequence of TS G holds
( not o ==> roots p or not t = o -tree p ) ; :: thesis: contradiction
A4: (TS G) \ {t} c= TS G by XBOOLE_1:36;
reconsider Y = (TS G) \ {t} as Subset of (FinTrees the carrier of G) ;
A5: now :: thesis: for d being Symbol of G st d in Terminals G holds
root-tree d in Y
let d be Symbol of G; :: thesis: ( d in Terminals G implies root-tree d in Y )
assume A6: d in Terminals G ; :: thesis: root-tree d in Y
then A7: root-tree d in TS G by DTCONSTR:def 1;
root-tree d <> t by A2, A6;
hence root-tree d in Y by A7, ZFMISC_1:56; :: thesis: verum
end;
now :: thesis: for o being Symbol of G
for p being FinSequence of Y st o ==> roots p holds
o -tree p in Y
let o be Symbol of G; :: thesis: for p being FinSequence of Y st o ==> roots p holds
o -tree p in Y
let p be FinSequence of Y; :: thesis: ( o ==> roots p implies o -tree p in Y )
rng p c= Y by FINSEQ_1:def 4;
then rng p c= TS G by A4;
then reconsider q = p as FinSequence of TS G by FINSEQ_1:def 4;
assume A8: o ==> roots p ; :: thesis: o -tree p in Y
then A9: o -tree q in TS G by DTCONSTR:def 1;
t <> o -tree q by A3, A8;
hence o -tree p in Y by A9, ZFMISC_1:56; :: thesis: verum
end;
then TS G c= Y by A5, DTCONSTR:def 1;
then t nin {t} by A1, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum