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)
now :: thesis: for x being object st x in meet (rng B) holds
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;
then A1: meet (rng B) c= Intersection B ;
Intersection B c= meet (rng B)
proof
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;
hence Intersection B = meet (rng B) by A1, XBOOLE_0:def 10; :: thesis: verum