hereby :: thesis: ( not the Sorts of U0 . s <> {} implies ex b_{1} being Subset of ( the Sorts of U0 . s) st b_{1} = {} )

assume
the Sorts of U0 . s = {}
; :: thesis: ex bassume
the Sorts of U0 . s <> {}
; :: thesis: ex E being Subset of ( the Sorts of U0 . s) ex A being non empty set st

( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )

then reconsider A = the Sorts of U0 . s as non empty set ;

set E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ;

{ a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } c= A

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } as Subset of ( the Sorts of U0 . s) ;

take E = E; :: thesis: ex A being non empty set st

( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )

take A = A; :: thesis: ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )

thus ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ; :: thesis: verum

end;( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )

then reconsider A = the Sorts of U0 . s as non empty set ;

set E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ;

{ a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } c= A

proof

then reconsider E = { a where a is Element of A : ex o being OperSymbol of S st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } or x in A )

assume x in { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ; :: thesis: x in A

then ex w being Element of the Sorts of U0 . s st

( w = x & ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & w in rng (Den (o,U0)) ) ) ;

hence x in A ; :: thesis: verum

end;( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } or x in A )

assume x in { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ; :: thesis: x in A

then ex w being Element of the Sorts of U0 . s st

( w = x & ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & w in rng (Den (o,U0)) ) ) ;

hence x in A ; :: thesis: verum

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } as Subset of ( the Sorts of U0 . s) ;

take E = E; :: thesis: ex A being non empty set st

( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )

take A = A; :: thesis: ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )

thus ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ; :: thesis: verum

take {} ( the Sorts of U0 . s) ; :: thesis: {} ( the Sorts of U0 . s) = {}

thus {} ( the Sorts of U0 . s) = {} ; :: thesis: verum