let X be set ; for L being List of X
for O being Operation of X
for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let L be List of X; for O being Operation of X
for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let O be Operation of X; for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let n be Nat; L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
thus
L WHEREge (O,(n + 1)) c= L WHEREgt (O,n)
XBOOLE_0:def 10 L WHEREgt (O,n) c= L WHEREge (O,(n + 1))
let z be object ; TARSKI:def 3 ( not z in L WHEREgt (O,n) or z in L WHEREge (O,(n + 1)) )
assume
z in L WHEREgt (O,n)
; z in L WHEREge (O,(n + 1))
then consider x being Element of X such that
A2:
( z = x & n in card (x . O) & x in L )
;
Segm (n + 1) = succ (Segm n)
by NAT_1:38;
then
n + 1 c= card (x . O)
by A2, ORDINAL1:21;
hence
z in L WHEREge (O,(n + 1))
by A2; verum