set E = { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ;

{ a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } c= the carrier of U0

( arity o = 0 & a in rng o ) } is Subset of U0 ; :: thesis: verum

( arity o = 0 & a in rng o ) } ;

{ a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } c= the carrier of U0

proof

hence
{ a where a is Element of U0 : ex o being operation of U0 st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } or x in the carrier of U0 )

assume x in { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ; :: thesis: x in the carrier of U0

then ex w being Element of U0 st

( w = x & ex o being operation of U0 st

( arity o = 0 & w in rng o ) ) ;

hence x in the carrier of U0 ; :: thesis: verum

end;( arity o = 0 & a in rng o ) } or x in the carrier of U0 )

assume x in { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ; :: thesis: x in the carrier of U0

then ex w being Element of U0 st

( w = x & ex o being operation of U0 st

( arity o = 0 & w in rng o ) ) ;

hence x in the carrier of U0 ; :: thesis: verum

( arity o = 0 & a in rng o ) } is Subset of U0 ; :: thesis: verum