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