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)

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

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

end;

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

end;

now :: thesis: for x being object holds

( x in Intersection F1 iff x in meet (rng F1) )

hence
Intersection F1 = meet (rng F1)
by TARSKI:2; :: thesis: verum( x in Intersection F1 iff x in meet (rng F1) )

let x be object ; :: 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, Th51;

hence ( x in Intersection F1 iff x in meet (rng F1) ) by A1, Th52; :: thesis: verum

end;( x in Intersection F1 iff for n being Nat st n in dom F1 holds

x in F1 . n ) by A1, Th51;

hence ( x in Intersection F1 iff x in meet (rng F1) ) by A1, Th52; :: thesis: verum