let L be complete LATTICE; :: thesis: for a being Element of L
for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ) holds
Sup <= a
let a be Element of L; :: thesis: for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ) holds
Sup <= a
let F be Function-yielding Function; :: thesis: ( ( for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ) implies Sup <= a )
assume A1: for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ; :: thesis: Sup <= a
rng (/\\ ((Frege F),L)) is_<=_than a

proof

let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in rng (/\\ ((Frege F),L)) or c <= a )
assume c in rng (/\\ ((Frege F),L)) ; :: thesis: c <= a
then consider f being object such that
A2: f in dom (Frege F) and
A3: c = //\ (((Frege F) . f),L) by Th13;
reconsider f = f as Function by A2;
f in dom (Frege F) by A2;
hence c <= a by A1, A3; :: thesis: verum

end;

then sup (rng (/\\ ((Frege F),L))) <= a by YELLOW_0:32;
hence Sup <= a by YELLOW_2:def 5; :: thesis: verum