let X be set ; :: thesis: for L being List of X
for O being Operation of X holds L WHEREgt (O,0) = L WHERE O
let L be List of X; :: thesis: for O being Operation of X holds L WHEREgt (O,0) = L WHERE O
let O be Operation of X; :: thesis: L WHEREgt (O,0) = L WHERE O
thus L WHEREgt (O,0) c= L WHERE O by Th8; :: according to XBOOLE_0:def 10 :: thesis: L WHERE O c= L WHEREgt (O,0)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE O or z in L WHEREgt (O,0) )
assume A1: z in L WHERE O ; :: thesis: z in L WHEREgt (O,0)
then reconsider z = z as Element of X ;
A2: ( z . O <> {} & z in L ) by A1, Th3;
then 0 in card (z . O) by ORDINAL3:8;
hence z in L WHEREgt (O,0) by A2; :: thesis: verum