let X be set ; for L being List of X
for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)
let L be List of X; for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)
let O be Operation of X; L WHEREeq (O,0) = L WHERE (NOT O)
thus
L WHEREeq (O,0) c= L WHERE (NOT O)
XBOOLE_0:def 10 L WHERE (NOT O) c= L WHEREeq (O,0)
let z be object ; TARSKI:def 3 ( not z in L WHERE (NOT O) or z in L WHEREeq (O,0) )
assume
z in L WHERE (NOT O)
; z in L WHEREeq (O,0)
then consider x being Element of X such that
A2:
( z = x & ex y being Element of X st
( x,y in NOT O & x in L ) )
;
consider y being Element of X such that
A3:
( x,y in NOT O & x in L )
by A2;
[x,y] in NOT O
by A3;
then
( x = y & x in X & x nin dom O )
by Th36;
then
x . O = {}
by RELAT_1:170;
then
card (x . O) = 0
;
hence
z in L WHEREeq (O,0)
by A2; verum