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

hence Sup <= a by YELLOW_2:def 5; :: thesis: verum

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

then
sup (rng (/\\ ((Frege F),L))) <= a
by YELLOW_0:32;
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;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

hence Sup <= a by YELLOW_2:def 5; :: thesis: verum