let L be non empty complete Poset; :: thesis: for p being Function of L,L st p is projection holds
Image p is complete
let p be Function of L,L; :: thesis: ( p is projection implies Image p is complete )
A1: the carrier of (Image p) = rng p by YELLOW_0:def 15;
assume A2: p is projection ; :: thesis: Image p is complete
then reconsider Lc = { c where c is Element of L : c <= p . c } , Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by Th43;
A3: ( the carrier of (subrelstr Lc) = Lc & rng p = Lc /\ Lk ) by A2, Th42, YELLOW_0:def 15;
p is monotone by A2;
then subrelstr Lc is sups-inheriting by Th49;
then A4: subrelstr Lc is complete LATTICE by YELLOW_2:31;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by A2, Th45;
A5: Image pc is infs-inheriting by A2, Th47, Th53;
A6: the carrier of (Image pc) = rng pc by YELLOW_0:def 15
.= the carrier of (Image p) by A2, A1, Th44 ;
then the InternalRel of (Image pc) = the InternalRel of (subrelstr Lc) |_2 the carrier of (Image p) by YELLOW_0:def 14
.= ( the InternalRel of L |_2 the carrier of (subrelstr Lc)) |_2 the carrier of (Image p) by YELLOW_0:def 14
.= the InternalRel of L |_2 the carrier of (Image p) by A1, A3, WELLORD1:22, XBOOLE_1:17
.= the InternalRel of (Image p) by YELLOW_0:def 14 ;
hence Image p is complete by A4, A5, A6, YELLOW_2:30; :: thesis: verum