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

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

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;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