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 Lk = { k where k is Element of L : p . k <= k } ;
set Lc = { c where c is Element of L : c <= p . c } ;
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 object ; :: 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 A2: 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 x9 = x as Element of L ;
A3: ex l being object st
( l in dom p & p . l = x ) by A2, FUNCT_1:def 3;
then p . x9 <= x9 by A1, YELLOW_2:18;
then A4: x in { k where k is Element of L : p . k <= k } ;
x9 <= p . x9 by A1, A3, YELLOW_2:18;
then x in { c where c is Element of L : c <= p . c } ;
hence x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by A4, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: 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 A5: 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 x in { c where c is Element of L : c <= p . c } by XBOOLE_0:def 4;
then A6: ex lc being Element of L st
( x = lc & lc <= p . lc ) ;
x in { k where k is Element of L : p . k <= k } by A5, XBOOLE_0:def 4;
then ex lk being Element of L st
( x = lk & p . lk <= lk ) ;
then ( dom p = the carrier of L & x = p . x ) by A6, FUNCT_2:def 1, ORDERS_2:2;
hence x in rng p by A6, FUNCT_1:def 3; :: thesis: verum