let L be non empty Poset; :: thesis: for k being Function of L,L st k is kernel holds
( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) ) ) )
let k be Function of L,L; :: thesis: ( k is kernel implies ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) ) ) ) )
assume A1: k is kernel ; :: thesis: ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) ) ) )
then [(corestr k),(inclusion k)] is Galois by Th42;
then corestr k is upper_adjoint by Def11;
hence A2: corestr k is infs-preserving ; :: thesis: for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) )
let X be Subset of L; :: thesis: ( X c= the carrier of (Image k) & ex_inf_of X,L implies ( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) ) )
assume that
A3: X c= the carrier of (Image k) and
A4: ex_inf_of X,L ; :: thesis: ( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) )
A5: corestr k preserves_inf_of X by A2, WAYBEL_0:def 32;
A6: corestr k = k by Th32;
A7: X c= rng k by A3, YELLOW_0:def 15;
k is projection by A1;
then k is idempotent by Def13;
then k .: X = X by A7, YELLOW_2:22;
hence ( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) ) by A4, A5, A6, WAYBEL_0:def 30; :: thesis: verum