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 monotone by A1, Def13;
A6: c is idempotent by A1, Def13;
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 A7: x in X ; :: thesis: c . (inf X) <= x
inf X is_<=_than X by A3, YELLOW_0:31;
then inf X <= x by A7, LATTICE3:def 8;
then c . (inf X) <= c . x by A5, Def2;
hence c . (inf X) <= x by A4, A6, A7, Lm2; :: thesis: verum

end;

then A8: c . (inf X) <= inf X by A3, YELLOW_0:31;
(id L) . (inf X) <= c . (inf X) by A2, YELLOW_2:9;
then inf X <= c . (inf X) by FUNCT_1:18;
hence inf X = c . (inf X) by A8, ORDERS_2:2; :: thesis: verum