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 )
assume A1: 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 Th46;
A2: p is monotone by A1, Def13;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by A1, Th48;
subrelstr Lc is sups-inheriting by A2, Th52;
then A3: subrelstr Lc is complete LATTICE by YELLOW_2:33;
pc is closure by A1, Th50;
then A4: Image pc is infs-inheriting by Th56;
A5: the carrier of (Image p) = rng p by YELLOW_0:def 15;
A6: the carrier of (subrelstr Lc) = Lc by YELLOW_0:def 15;
A7: rng p = Lc /\ Lk by A1, Th45;
A8: the carrier of (Image pc) = rng pc by YELLOW_0:def 15
.= the carrier of (Image p) by A1, A5, Th47 ;
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 A5, A6, A7, WELLORD1:29, XBOOLE_1:17
.= the InternalRel of (Image p) by YELLOW_0:def 14 ;
hence Image p is complete by A3, A4, A8, YELLOW_2:32; :: thesis: verum