let X be set ; :: thesis: for B being SetSequence of X holds Intersection B = meet (rng B)

let B be SetSequence of X; :: thesis: Intersection B = meet (rng B)

Intersection B c= meet (rng B)

let B be SetSequence of X; :: thesis: Intersection B = meet (rng B)

now :: thesis: for x being object st x in meet (rng B) holds

x in Intersection B

then A1:
meet (rng B) c= Intersection B
;x in Intersection B

let x be object ; :: thesis: ( x in meet (rng B) implies x in Intersection B )

assume x in meet (rng B) ; :: thesis: x in Intersection B

then for n being Nat holds x in B . n by Th7;

hence x in Intersection B by PROB_1:13; :: thesis: verum

end;assume x in meet (rng B) ; :: thesis: x in Intersection B

then for n being Nat holds x in B . n by Th7;

hence x in Intersection B by PROB_1:13; :: thesis: verum

Intersection B c= meet (rng B)

proof

hence
Intersection B = meet (rng B)
by A1, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection B or x in meet (rng B) )

assume x in Intersection B ; :: thesis: x in meet (rng B)

then for n being Nat holds x in B . n by PROB_1:13;

hence x in meet (rng B) by Th7; :: thesis: verum

end;assume x in Intersection B ; :: thesis: x in meet (rng B)

then for n being Nat holds x in B . n by PROB_1:13;

hence x in meet (rng B) by Th7; :: thesis: verum