let L be non empty Poset; :: thesis: for k being Function of L,L
for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)
let k be Function of L,L; :: thesis: for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)
let X be Subset of L; :: thesis: ( k is kernel & ex_sup_of X,L & X c= rng k implies sup X = k . (sup X) )
assume that
A1: k is projection and
A2: k <= id L and
A3: ex_sup_of X,L and
A4: X c= rng k ; :: according to WAYBEL_1:def 15 :: thesis: sup X = k . (sup X)
A5: k is idempotent by A1, Def13;
A6: k is monotone by A1, Def13;
(id L) . (sup X) >= k . (sup X) by A2, YELLOW_2:10;
then A7: sup X >= k . (sup X) by TMAP_1:91;
k . (sup X) is_>=_than X

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= k . (sup X) )
assume A8: x in X ; :: thesis: x <= k . (sup X)
sup X is_>=_than X by A3, YELLOW_0:30;
then sup X >= x by A8, LATTICE3:def 9;
then k . (sup X) >= k . x by A6, Def2;
hence x <= k . (sup X) by A4, A5, A8, Lm2; :: thesis: verum

end;

then k . (sup X) >= sup X by A3, YELLOW_0:30;
hence sup X = k . (sup X) by A7, ORDERS_2:25; :: thesis: verum