let L be non empty Poset; :: thesis: for p being Function of L,L st p is projection holds
rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
let p be Function of L,L; :: thesis: ( p is projection implies rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } )
assume that
A1: p is idempotent and
p is monotone ; :: according to WAYBEL_1:def 13 :: thesis: rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
set Lc = { c where c is Element of L : c <= p . c } ;
set Lk = { k where k is Element of L : p . k <= k } ;
A2: dom p = the carrier of L by FUNCT_2:def 1;
thus rng p c= { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } :: according to XBOOLE_0:def 10 :: thesis: { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } c= rng p

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } )
assume A3: x in rng p ; :: thesis: x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
then reconsider x' = x as Element of L ;
consider l being set such that
A4: l in dom p and
A5: p . l = x by A3, FUNCT_1:def 5;
( x' <= p . x' & p . x' <= x' ) by A1, A4, A5, YELLOW_2:20;
then ( x in { c where c is Element of L : c <= p . c } & x in { k where k is Element of L : p . k <= k } ) ;
hence x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } or x in rng p )
assume x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } ; :: thesis: x in rng p
then A6: ( x in { c where c is Element of L : c <= p . c } & x in { k where k is Element of L : p . k <= k } ) by XBOOLE_0:def 4;
then consider lc being Element of L such that
A7: ( x = lc & lc <= p . lc ) ;
consider lk being Element of L such that
A8: ( x = lk & p . lk <= lk ) by A6;
x = p . x by A7, A8, ORDERS_2:25;
hence x in rng p by A2, A7, FUNCT_1:def 5; :: thesis: verum