let L be non empty Poset; :: thesis: for c being Function of L,L
for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)
let c be Function of L,L; :: thesis: for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)
let X be Subset of L; :: thesis: ( c is closure & ex_inf_of X,L & X c= rng c implies inf X = c . (inf X) )
assume that
A1: c is projection and
A2: id L <= c and
A3: ex_inf_of X,L and
A4: X c= rng c ; :: according to WAYBEL_1:def 14 :: thesis: inf X = c . (inf X)
A5: c is idempotent by A1, Def13;
A6: c is monotone by A1, Def13;
(id L) . (inf X) <= c . (inf X) by A2, YELLOW_2:10;
then A7: inf X <= c . (inf X) by TMAP_1:91;
c . (inf X) is_<=_than X

proof

let x be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not x in X or c . (inf X) <= x )
assume A8: x in X ; :: thesis: c . (inf X) <= x
inf X is_<=_than X by A3, YELLOW_0:31;
then inf X <= x by A8, LATTICE3:def 8;
then c . (inf X) <= c . x by A6, Def2;
hence c . (inf X) <= x by A4, A5, A8, Lm2; :: thesis: verum

end;

then c . (inf X) <= inf X by A3, YELLOW_0:31;
hence inf X = c . (inf X) by A7, ORDERS_2:25; :: thesis: verum