let L be complete LATTICE; :: thesis: for J being non empty set
for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
let J be non empty set ; :: thesis: for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
let j be Element of J; :: thesis: for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
let F be Function of J, the carrier of L; :: thesis: ( F . j <= Sup & Inf <= F . j )
F . j in rng F by FUNCT_2:4;
hence ( F . j <= Sup & Inf <= F . j ) by Th22; :: thesis: verum