hereby :: thesis: ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} )
assume 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
proof
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;
then reconsider 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)) ) } 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;
assume the Sorts of U0 . s = {} ; :: thesis: ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {}
take {} ( the Sorts of U0 . s) ; :: thesis: {} ( the Sorts of U0 . s) = {}
thus {} ( the Sorts of U0 . s) = {} ; :: thesis: verum