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 object ; :: 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 and
A2: ex o being operation of U0 st
( arity o = 0 & u in rng o ) ;
consider o being operation of U0 such that
A3: arity o = 0 and
A4: u in rng o by A2;
consider a2 being object such that
A5: a2 in dom o and
A6: u = o . a2 by A4, FUNCT_1:def 3;
dom o = 0 -tuples_on the carrier of U0 by A3, MARGREL1:22;
then a2 is Tuple of 0 , the carrier of U0 by A5, FINSEQ_2:131;
then reconsider a1 = a2 as FinSequence of the carrier of U0 ;
len a1 = 0 by A3, A5, MARGREL1:def 25;
then a1 = {} ;
hence a in { (o . {}) where o is operation of U0 : arity o = 0 } by A1, A3, A6; :: thesis: verum

end;

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

proof

let a be object ; :: 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
A7: a = o . {} and
A8: arity o = 0 ;
dom o = 0 -tuples_on the carrier of U0 by A8, MARGREL1:22
.= {(<*> the carrier of U0)} by FINSEQ_2:94 ;
then {} the carrier of U0 in dom o by TARSKI:def 1;
then o . ({} the carrier of U0) in rng o by FUNCT_1:def 3;
hence a in Constants U0 by A7, A8; :: thesis: verum

end;