let L be complete LATTICE; :: thesis: for k being kernel Function of L,L holds
( corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
let k be kernel Function of L,L; :: thesis: ( corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
A1: [(corestr k),(inclusion k)] is Galois by WAYBEL_1:39;
then A2: inclusion k is lower_adjoint ;
A3: corestr k is upper_adjoint by A1;
hence ( corestr k is infs-preserving & inclusion k is sups-preserving ) by A2; :: thesis: ( LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
thus ( LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k ) by A1, A2, A3, Def1, Def2; :: thesis: verum