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 set ; :: 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 set ; :: 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, Def1;
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