let U0 be Universal_Algebra; :: thesis: Constants U0 = { (o . {} ) where o is operation of U0 : arity o = 0 }
set S = { (o . {} ) where o is operation of U0 : arity o = 0 } ;
thus Constants U0 c= { (o . {} ) where o is operation of U0 : arity o = 0 } :: according to XBOOLE_0:def 10 :: thesis: { (o . {} ) where o is operation of U0 : arity o = 0 } c= Constants U0

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Constants U0 or a in { (o . {} ) where o is operation of U0 : arity o = 0 } )
assume a in Constants U0 ; :: thesis: a in { (o . {} ) where o is operation of U0 : arity o = 0 }
then consider u being Element of U0 such that
A1: ( u = a & ex o being operation of U0 st
( arity o = 0 & u in rng o ) ) ;
consider o being operation of U0 such that
A2: arity o = 0 and
A3: u in rng o by A1;
consider a2 being set such that
A4: ( a2 in dom o & u = o . a2 ) by A3, FUNCT_1:def 5;
dom o = 0 -tuples_on the carrier of U0 by A2, UNIALG_2:2;
then a2 = <*> the carrier of U0 by A4, FINSEQ_2:113;
then reconsider a1 = a2 as FinSequence of the carrier of U0 ;
len a1 = 0 by A2, A4, UNIALG_1:def 10;
then a1 = {} ;
hence a in { (o . {} ) where o is operation of U0 : arity o = 0 } by A1, A2, A4; :: thesis: verum

end;

thus { (o . {} ) where o is operation of U0 : arity o = 0 } c= Constants U0 :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (o . {} ) where o is operation of U0 : arity o = 0 } or a in Constants U0 )
assume a in { (o . {} ) where o is operation of U0 : arity o = 0 } ; :: thesis: a in Constants U0
then consider o being operation of U0 such that
A5: ( a = o . {} & arity o = 0 ) ;
dom o = 0 -tuples_on the carrier of U0 by A5, UNIALG_2:2
.= {(<*> the carrier of U0)} by FINSEQ_2:112 ;
then {} the carrier of U0 in dom o by TARSKI:def 1;
then A6: ( o . ({} the carrier of U0) in rng o & rng o c= the carrier of U0 ) by FUNCT_1:def 5;
thus a in Constants U0 by A5, A6; :: thesis: verum

end;