let X be set ; :: thesis: for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)
let F1 be FinSequence of bool X; :: thesis: Intersection F1 = meet (rng F1)

per cases ( F1 <> {} or F1 = {} ) ;

suppose A1: F1 <> {} ; :: thesis: Intersection F1 = meet (rng F1)

now

let x be set ; :: thesis: ( x in Intersection F1 iff x in meet (rng F1) )
( x in Intersection F1 iff for n being Nat st n in dom F1 holds
x in F1 . n ) by A1, Th56;
hence ( x in Intersection F1 iff x in meet (rng F1) ) by A1, Th57; :: thesis: verum

end;

hence Intersection F1 = meet (rng F1) by TARSKI:1; :: thesis: verum

end;

suppose F1 = {} ; :: thesis: Intersection F1 = meet (rng F1)

hence Intersection F1 = meet (rng F1) by Def9, RELAT_1:38, SETFAM_1:1; :: thesis: verum

end;

end;