let A be Universal_Algebra; :: thesis: for B being Subset of A holds Constants A c= B |^ 1
let B be Subset of A; :: thesis: Constants A c= B |^ 1
let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin Constants A or not x nin B |^ 1 )
assume x in Constants A ; :: thesis: not x nin B |^ 1
then consider a being Element of A such that
A1: ( x = a & ex o being Element of Operations A st
( arity o = 0 & a in rng o ) ) ;
consider o being Element of Operations A such that
A2: ( arity o = 0 & a in rng o ) by A1;
consider s being set such that
A3: ( s in dom o & a = o . s ) by A2, FUNCT_1:def 5;
consider z being set such that
A4: ( z in dom the charact of A & o = the charact of A . z ) by FUNCT_1:def 5;
reconsider z = z as Element of dom the charact of A by A4;
A5: Den z,A = o by A4;
A6: s is Element of 0 -tuples_on the carrier of A by A3, A2, UNIALG_2:2;
reconsider s = s as Element of the carrier of A * by A3;
len s = 0 by A6, FINSEQ_1:def 18;
then s = {} ;
then rng s c= B by RELAT_1:60, XBOOLE_1:2;
then A7: x in { ((Den r,A) . p) where r is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den r,A) & rng p c= B ) } by A1, A3, A5;
B |^ 0 = B by Th18;
then B |^ (0 + 1) = B \/ { ((Den r,A) . p) where r is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den r,A) & rng p c= B ) } by Th19;
hence not x nin B |^ 1 by A7, XBOOLE_0:def 3; :: thesis: verum