let G be non empty DTConstrStr ; :: thesis: (Terminals G) \/ (NonTerminals G) = the carrier of G
thus (Terminals G) \/ (NonTerminals G) c= the carrier of G :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= (Terminals G) \/ (NonTerminals G)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (Terminals G) \/ (NonTerminals G) or a in the carrier of G )
assume a in (Terminals G) \/ (NonTerminals G) ; :: thesis: a in the carrier of G
then ( a in Terminals G or a in NonTerminals G ) by XBOOLE_0:def 3;
then ( ex s being Symbol of G st
( a = s & ( for n being FinSequence holds not s ==> n ) ) or ex s being Symbol of G st
( a = s & ex n being FinSequence st s ==> n ) ) ;
hence a in the carrier of G ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of G or a in (Terminals G) \/ (NonTerminals G) )
assume a in the carrier of G ; :: thesis: a in (Terminals G) \/ (NonTerminals G)
then reconsider s = a as Symbol of G ;
( for n being FinSequence holds not s ==> n or ex n being FinSequence st s ==> n ) ;
then ( a in Terminals G or a in NonTerminals G ) ;
hence a in (Terminals G) \/ (NonTerminals G) by XBOOLE_0:def 3; :: thesis: verum