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 monotone by A1;
A6: k is idempotent by A1;
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 A7: x in X ; :: thesis: x <= k . (sup X)
sup X is_>=_than X by A3, YELLOW_0:30;
then sup X >= x by A7;
then k . (sup X) >= k . x by A5;
hence x <= k . (sup X) by A4, A6, A7, Lm2; :: thesis: verum
end;
then A8: k . (sup X) >= sup X by A3, YELLOW_0:30;
(id L) . (sup X) >= k . (sup X) by A2, YELLOW_2:9;
then sup X >= k . (sup X) ;
hence sup X = k . (sup X) by A8, ORDERS_2:2; :: thesis: verum