let X be set ; :: thesis: for F being SetSequence of X
for x being object holds
( x in meet F iff for z being Nat holds x in F . z )
let F be SetSequence of X; :: thesis: for x being object holds
( x in meet F iff for z being Nat holds x in F . z )
let x be object ; :: thesis: ( x in meet F iff for z being Nat holds x in F . z )
hereby :: thesis: ( ( for z being Nat holds x in F . z ) implies x in meet F )
assume A1: x in meet F ; :: thesis: for z being Nat holds x in F . z
let z be Nat; :: thesis: x in F . z
z in NAT by ORDINAL1:def 12;
then z in dom F by FUNCT_2:def 1;
hence x in F . z by A1, FUNCT_6:25; :: thesis: verum
end;
assume for z being Nat holds x in F . z ; :: thesis: x in meet F
then for y being object st y in dom F holds
x in F . y ;
hence x in meet F by FUNCT_6:25; :: thesis: verum