let a be set ; :: thesis: Lang (EmptyGrammar a) = {{}}
set E = EmptyGrammar a;
A1: Terminals (EmptyGrammar a) = {} by Th10;
thus Lang (EmptyGrammar a) c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= Lang (EmptyGrammar a)

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Lang (EmptyGrammar a) or b in {{}} )
assume b in Lang (EmptyGrammar a) ; :: thesis: b in {{}}
then ex p being String of (EmptyGrammar a) st
( b = p & rng p c= Terminals (EmptyGrammar a) & p is_derivable_from <* the InitialSym of (EmptyGrammar a)*> ) ;
then b = {} by A1;
hence b in {{}} by TARSKI:def 1; :: thesis: verum

end;

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in {{}} or b in Lang (EmptyGrammar a) )
assume b in {{}} ; :: thesis: b in Lang (EmptyGrammar a)
then A2: b = {} by TARSKI:def 1;
the Rules of (EmptyGrammar a) = {[a,{}]} by Def7;
then A3: [a,{}] in the Rules of (EmptyGrammar a) by TARSKI:def 1;
the carrier of (EmptyGrammar a) = {a} by Def7;
then a = the InitialSym of (EmptyGrammar a) by TARSKI:def 1;
then the InitialSym of (EmptyGrammar a) ==> <*> the carrier of (EmptyGrammar a) by A3;
then A4: <*> the carrier of (EmptyGrammar a) is_derivable_from <* the InitialSym of (EmptyGrammar a)*> by Th3, Th7;
rng {} = {} ;
hence b in Lang (EmptyGrammar a) by A1, A2, A4; :: thesis: verum