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)) ) ) ) )
A1: corestr k = k by Th30;
assume A2: 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 A3: k is idempotent by Def13;
[(corestr k),(inclusion k)] is Galois by A2, Th39;
then A4: corestr k is upper_adjoint ;
hence 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
A5: X c= the carrier of (Image k) and
A6: ex_inf_of X,L ; :: thesis: ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) )
X c= rng k by A5, YELLOW_0:def 15;
then A7: k .: X = X by A3, YELLOW_2:20;
corestr k preserves_inf_of X by A4, WAYBEL_0:def 32;
hence ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) by A6, A1, A7; :: thesis: verum