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