let L be non empty transitive RelStr ; :: thesis: for k being Function of L,L st k is filtered-infs-preserving holds
corestr k is filtered-infs-preserving
let k be Function of L,L; :: thesis: ( k is filtered-infs-preserving implies corestr k is filtered-infs-preserving )
assume A1: k is filtered-infs-preserving ; :: thesis: corestr k is filtered-infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def 36 :: thesis: ( X is empty or not X is filtered or corestr k preserves_inf_of X )
assume ( not X is empty & X is filtered ) ; :: thesis: corestr k preserves_inf_of X
then A2: k preserves_inf_of X by A1, WAYBEL_0:def 36;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:32;
assume A4: 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) )
then A5: ex_inf_of k .: X,L by A2, WAYBEL_0:def 30;
A6: inf (k .: X) = k . (inf X) by A2, A4, WAYBEL_0:def 30;
A7: dom k = the carrier of L by FUNCT_2:def 1;
A8: rng k = the carrier of (Image k) by YELLOW_0:def 15;
A9: k . (inf X) in rng k by A7, FUNCT_1:def 5;
reconsider fX = (corestr k) .: X as Subset of (Image k) ;
"/\" fX,L is Element of (Image k) by A2, A3, A4, A8, A9, WAYBEL_0:def 30;
hence ex_inf_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:64; :: thesis: "/\" ((corestr k) .: X),(Image k) = (corestr k) . ("/\" X,L)
thus "/\" ((corestr k) .: X),(Image k) = (corestr k) . ("/\" X,L) by A3, A5, A6, YELLOW_0:64; :: thesis: verum