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 F . j <= a ) holds
Sup <= a
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 F . j <= a ) holds
Sup <= a
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 F . j <= a ) holds
Sup <= a
let F be Function of J, the carrier of L; :: thesis: ( ( for j being Element of J holds F . j <= a ) implies Sup <= a )
assume A1: for j being Element of J holds F . j <= a ; :: thesis: Sup <= a

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

let c be Element of L; :: thesis: ( c in rng F implies c <= a )
assume c in rng F ; :: thesis: c <= a
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 c <= a by A1; :: thesis: verum

end;

then rng F is_<=_than a ;
hence Sup <= a by YELLOW_0:32; :: thesis: verum