let f be SetSequence of X; :: thesis: ( f = inferior_setsequence A iff for n being Nat holds f . n = Intersection (A ^\ n) )
thus ( f = inferior_setsequence A implies for n being Nat holds f . n = Intersection (A ^\ n) ) :: thesis: ( ( for n being Nat holds f . n = Intersection (A ^\ n) ) implies f = inferior_setsequence A )

proof

assume AA: f = inferior_setsequence A ; :: thesis: for n being Nat holds f . n = Intersection (A ^\ n)
let n be Nat; :: thesis: f . n = Intersection (A ^\ n)
for x being object holds
( x in (inferior_setsequence A) . n iff x in Intersection (A ^\ n) )

proof

let x be object ; :: thesis: ( x in (inferior_setsequence A) . n iff x in Intersection (A ^\ n) )

hereby :: thesis: ( x in Intersection (A ^\ n) implies x in (inferior_setsequence A) . n )

assume A3: x in (inferior_setsequence A) . n ; :: thesis: x in Intersection (A ^\ n)
for k being Nat holds x in (A ^\ n) . k

proof

let k be Nat; :: thesis: x in (A ^\ n) . k
x in A . (k + n) by A3, SETLIM_1:19;
hence x in (A ^\ n) . k by NAT_1:def 3; :: thesis: verum

end;

hence x in Intersection (A ^\ n) by PROB_1:13; :: thesis: verum

end;

assume A5: x in Intersection (A ^\ n) ; :: thesis: x in (inferior_setsequence A) . n
for k being Nat holds x in A . (n + k)

proof

let k be Nat; :: thesis: x in A . (n + k)
x in (A ^\ n) . k by A5, PROB_1:13;
hence x in A . (n + k) by NAT_1:def 3; :: thesis: verum

end;

hence x in (inferior_setsequence A) . n by SETLIM_1:19; :: thesis: verum

end;

hence f . n = Intersection (A ^\ n) by AA, TARSKI:2; :: thesis: verum

end;

assume B1: for n being Nat holds f . n = Intersection (A ^\ n) ; :: thesis: f = inferior_setsequence A
for n being Element of NAT holds f . n = (inferior_setsequence A) . n

proof

let n be Element of NAT ; :: thesis: f . n = (inferior_setsequence A) . n
for x being object holds
( x in f . n iff x in (inferior_setsequence A) . n )

proof

let x be object ; :: thesis: ( x in f . n iff x in (inferior_setsequence A) . n )

hereby :: thesis: ( x in (inferior_setsequence A) . n implies x in f . n )

assume x in f . n ; :: thesis: x in (inferior_setsequence A) . n
then A5: x in Intersection (A ^\ n) by B1;
for k being Nat holds x in A . (n + k)

proof

let k be Nat; :: thesis: x in A . (n + k)
x in (A ^\ n) . k by A5, PROB_1:13;
hence x in A . (n + k) by NAT_1:def 3; :: thesis: verum

end;

hence x in (inferior_setsequence A) . n by SETLIM_1:19; :: thesis: verum

end;

assume A3: x in (inferior_setsequence A) . n ; :: thesis: x in f . n
for k being Nat holds x in (A ^\ n) . k

proof

let k be Nat; :: thesis: x in (A ^\ n) . k
x in A . (k + n) by A3, SETLIM_1:19;
hence x in (A ^\ n) . k by NAT_1:def 3; :: thesis: verum

end;

then x in Intersection (A ^\ n) by PROB_1:13;
hence x in f . n by B1; :: thesis: verum

end;

hence f . n = (inferior_setsequence A) . n by TARSKI:2; :: thesis: verum

end;

then f = inferior_setsequence A ;
hence f = inferior_setsequence A ; :: thesis: verum