let G be non empty ManySortedSign ; :: thesis: SortsWithConstants G c= InnerVertices G

per cases ( G is void or not G is void ) ;

suppose G is void ; :: thesis: SortsWithConstants G c= InnerVertices G

hence SortsWithConstants G c= InnerVertices G by Def1; :: thesis: verum

end;

suppose A1: not G is void ; :: thesis: SortsWithConstants G c= InnerVertices G

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SortsWithConstants G or x in InnerVertices G )
assume A2: x in SortsWithConstants G ; :: thesis: x in InnerVertices G
SortsWithConstants G = { v where v is SortSymbol of G : v is with_const_op } by A1, Def1;
then consider x9 being SortSymbol of G such that
A3: x9 = x and
A4: x9 is with_const_op by A2;
ex o being OperSymbol of G st
( the Arity of G . o = {} & the ResultSort of G . o = x9 ) by A4;
hence x in InnerVertices G by A1, A3, FUNCT_2:4; :: thesis: verum

end;

end;