let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
let X be set ; :: thesis: for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
let A1 be SetSequence of X; :: thesis: (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
reconsider Y = { (A1 . k) where k is Nat : n <= k } as Subset-Family of X by SETLIM_1:28;
(inferior_setsequence A1) . n = meet Y by SETLIM_1:def 2
.= meet (rng (A1 ^\ n)) by SETLIM_1:6 ;
hence (inferior_setsequence A1) . n = Intersection (A1 ^\ n) by SETLIM_1:8; :: thesis: verum