let L be non empty transitive RelStr ; :: thesis: for k being Function of L,L st k is infs-preserving holds
corestr k is infs-preserving
let k be Function of L,L; :: thesis: ( k is infs-preserving implies corestr k is infs-preserving )
assume A1: k is infs-preserving ; :: thesis: corestr k is infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def 32 :: thesis: corestr k preserves_inf_of X
assume A2: ex_inf_of X,L ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (corestr k) .: X, Image k & "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) )
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
A4: k preserves_inf_of X by A1;
then A5: ex_inf_of k .: X,L by A2;
reconsider fX = (corestr k) .: X as Subset of (Image k) ;
dom k = the carrier of L by FUNCT_2:def 1;
then ( rng k = the carrier of (Image k) & k . (inf X) in rng k ) by FUNCT_1:def 3, YELLOW_0:def 15;
then "/\" (fX,L) is Element of (Image k) by A4, A3, A2;
hence ex_inf_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:63; :: thesis: "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L))
inf (k .: X) = k . (inf X) by A4, A2;
hence "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) by A3, A5, YELLOW_0:63; :: thesis: verum