let A be Universal_Algebra; for B being Subset of A holds Constants A c= B |^ 1
let B be Subset of A; Constants A c= B |^ 1
let x be object ; TARSKI:def 3 ( x nin Constants A or not x nin B |^ 1 )
assume
x in Constants A
; not x nin B |^ 1
then consider a being Element of A such that
A1:
x = a
and
A2:
ex o being Element of Operations A st
( arity o = 0 & a in rng o )
;
consider o being Element of Operations A such that
A3:
arity o = 0
and
A4:
a in rng o
by A2;
consider s being object such that
A5:
s in dom o
and
A6:
a = o . s
by A4, FUNCT_1:def 3;
consider z being object such that
A7:
z in dom the charact of A
and
A8:
o = the charact of A . z
by FUNCT_1:def 3;
reconsider z = z as Element of dom the charact of A by A7;
A9:
Den (z,A) = o
by A8;
A10:
s is Element of 0 -tuples_on the carrier of A
by A3, A5, MARGREL1:22;
reconsider s = s as Element of the carrier of A * by A5;
rng s c= B
by A10;
then A11:
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, A5, A6, A9;
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 A11, XBOOLE_0:def 3; verum