let X be set ; :: thesis: for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B
let B be SetSequence of X; :: thesis: (inferior_setsequence B) . 0 = Intersection B
(inferior_setsequence B) . 0 = meet { (B . k) where k is Element of NAT : k >= 0 } by def2
.= meet (rng B) by Th10
.= Intersection B by Th16 ;
hence (inferior_setsequence B) . 0 = Intersection B ; :: thesis: verum