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 set ; :: according to TARSKI:def 3 :: thesis: ( x nin Constants A or not x nin B )
assume x in Constants A ; :: thesis: not x nin B
then consider a being Element of A such that
A2: ( 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
A3: ( arity o = 0 & a in rng o ) by A2;
consider s being set such that
A4: ( s in dom o & a = o . s ) by A3, FUNCT_1:def 5;
A5: dom o = 0 -tuples_on the carrier of A by A3, UNIALG_2:2;
reconsider s = s as Element of the carrier of A * by A4;
A6: len s = 0 by A4, A5, FINSEQ_1:def 18;
then s = {} ;
then rng s c= B by RELAT_1:60, XBOOLE_1:2;
then ( s is FinSequence of B & B is_closed_on o ) by A1, FINSEQ_1:def 4, UNIALG_2:def 5;
hence not x nin B by A2, A3, A4, A6, UNIALG_2:def 4; :: thesis: verum