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:42;
then ( inclusion k is lower_adjoint & corestr k is upper_adjoint ) by WAYBEL_1:def 11, WAYBEL_1:def 12;
hence ( corestr k is infs-preserving & inclusion k is sups-preserving ) ; :: thesis: ( LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k )
hence ( LowerAdj (corestr k) = inclusion k & UpperAdj (inclusion k) = corestr k ) by A1, Def1, Def2; :: thesis: verum