let A be Universal_Algebra; :: thesis: for a being Element of A holds
( a in Generators A iff for o being Element of Operations A holds not a in rng o )
set Z = { (rng o) where o is Element of Operations A : verum } ;
let a be Element of A; :: thesis: ( a in Generators A iff for o being Element of Operations A holds not a in rng o )
hereby :: thesis: ( ( for o being Element of Operations A holds not a in rng o ) implies a in Generators A )
assume a in Generators A ; :: thesis: for o being Element of Operations A holds not a in rng o
then A1: a nin union { (rng o) where o is Element of Operations A : verum } by XBOOLE_0:def 5;
given o being Element of Operations A such that A2: a in rng o ; :: thesis: contradiction
rng o in { (rng o) where o is Element of Operations A : verum } ;
hence contradiction by A1, A2, TARSKI:def 4; :: thesis: verum
end;
assume A3: for o being Element of Operations A holds not a in rng o ; :: thesis: a in Generators A
assume a nin Generators A ; :: thesis: contradiction
then a in union { (rng o) where o is Element of Operations A : verum } by XBOOLE_0:def 5;
then consider X being set such that
A4: a in X and
A5: X in { (rng o) where o is Element of Operations A : verum } by TARSKI:def 4;
ex o being Element of Operations A st X = rng o by A5;
hence contradiction by A3, A4; :: thesis: verum