let L be complete LATTICE; :: thesis: for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
let a be Element of L; :: thesis: for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
let J be non empty set ; :: thesis: for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
let F be Function of J, the carrier of L; :: thesis: ( ( for j being Element of J holds a <= F . j ) implies a <= Inf )
assume A1: for j being Element of J holds a <= F . j ; :: thesis: a <= Inf

now :: thesis: for c being Element of L st c in rng F holds
a <= c

let c be Element of L; :: thesis: ( c in rng F implies a <= c )
assume c in rng F ; :: thesis: a <= c
then consider j being object such that
A2: j in dom F and
A3: c = F . j by FUNCT_1:def 3;
reconsider j = j as Element of J by A2;
c = F . j by A3;
hence a <= c by A1; :: thesis: verum

end;

then a is_<=_than rng F ;
hence a <= Inf by YELLOW_0:33; :: thesis: verum