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 () holds
//\ ((() . 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 () holds
//\ ((() . f),L) <= a ) holds
Sup <= a

let F be Function-yielding Function; :: thesis: ( ( for f being Function st f in dom () holds
//\ ((() . f),L) <= a ) implies Sup <= a )

assume A1: for f being Function st f in dom () holds
//\ ((() . f),L) <= a ; :: thesis:
rng (/\\ ((),L)) is_<=_than a
proof
let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in rng (/\\ ((),L)) or c <= a )
assume c in rng (/\\ ((),L)) ; :: thesis: c <= a
then consider f being object such that
A2: f in dom () and
A3: c = //\ ((() . f),L) by Th13;
reconsider f = f as Function by A2;
f in dom () by A2;
hence c <= a by A1, A3; :: thesis: verum
end;
then sup (rng (/\\ ((),L))) <= a by YELLOW_0:32;
hence Sup <= a by YELLOW_2:def 5; :: thesis: verum