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 Nat : k >= 0 } by Def2

.= meet (rng B) by Th5

.= Intersection B by Th8 ;

hence (inferior_setsequence B) . 0 = Intersection B ; :: thesis: verum

let B be SetSequence of X; :: thesis: (inferior_setsequence B) . 0 = Intersection B

(inferior_setsequence B) . 0 = meet { (B . k) where k is Nat : k >= 0 } by Def2

.= meet (rng B) by Th5

.= Intersection B by Th8 ;

hence (inferior_setsequence B) . 0 = Intersection B ; :: thesis: verum