let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let n be Nat; :: thesis: L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
thus L WHEREge (O,(n + 1)) c= L WHEREgt (O,n) :: according to XBOOLE_0:def 10 :: thesis: L WHEREgt (O,n) c= L WHEREge (O,(n + 1))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHEREge (O,(n + 1)) or z in L WHEREgt (O,n) )
assume z in L WHEREge (O,(n + 1)) ; :: thesis: z in L WHEREgt (O,n)
then consider x being Element of X such that
A1: ( z = x & n + 1 c= card (x . O) & x in L ) ;
Segm (n + 1) = succ (Segm n) by NAT_1:38;
then n in card (x . O) by A1, ORDINAL1:21;
hence z in L WHEREgt (O,n) by A1; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHEREgt (O,n) or z in L WHEREge (O,(n + 1)) )
assume z in L WHEREgt (O,n) ; :: thesis: 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; :: thesis: verum