let X be non empty set ; :: thesis: for F being SetSequence of X
for n being Element of NAT holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
let F be SetSequence of X; :: thesis: for n being Element of NAT holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
let n be Element of NAT ; :: thesis: ( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
{ (F . k) where k is Nat : n <= k } = rng (F ^\ n) by SETLIM_1:6;
hence (superior_setsequence F) . n = union (rng (F ^\ n)) by SETLIM_1:def 3; :: thesis: (inferior_setsequence F) . n = meet (rng (F ^\ n))
(inferior_setsequence F) . n = meet { (F . k) where k is Nat : n <= k } by SETLIM_1:def 2;
hence (inferior_setsequence F) . n = meet (rng (F ^\ n)) by SETLIM_1:6; :: thesis: verum