let A be Universal_Algebra; for B being Subset of A st B is opers_closed holds
Constants A c= B
let B be Subset of A; ( B is opers_closed implies Constants A c= B )
assume A1:
B is opers_closed
; Constants A c= B
let x be object ; TARSKI:def 3 ( x nin Constants A or not x nin B )
assume
x in Constants A
; not x nin B
then consider a being Element of A such that
A2:
x = a
and
A3:
ex o being Element of Operations A st
( arity o = 0 & a in rng o )
;
consider o being Element of Operations A such that
A4:
arity o = 0
and
A5:
a in rng o
by A3;
consider s being object such that
A6:
s in dom o
and
A7:
a = o . s
by A5, FUNCT_1:def 3;
A8:
dom o = 0 -tuples_on the carrier of A
by A4, MARGREL1:22;
reconsider s = s as Element of the carrier of A * by A6;
A9:
len s = 0
by A6, A8;
s = {}
by A6, A8;
then
rng s c= B
;
then A10:
s is FinSequence of B
by FINSEQ_1:def 4;
B is_closed_on o
by A1;
hence
not x nin B
by A2, A4, A7, A9, A10; verum