let L be non empty Poset; for p being Function of L,L st p is projection holds
( { c where c is Element of : c <= p . c } is non empty Subset of & { k where k is Element of : p . k <= k } is non empty Subset of )
let p be Function of L,L; ( p is projection implies ( { c where c is Element of : c <= p . c } is non empty Subset of & { k where k is Element of : p . k <= k } is non empty Subset of ) )
assume A1:
p is projection
; ( { c where c is Element of : c <= p . c } is non empty Subset of & { k where k is Element of : p . k <= k } is non empty Subset of )
defpred S1[ Element of ] means p . $1 <= $1;
defpred S2[ Element of ] means $1 <= p . $1;
set Lc = { c where c is Element of : S2[c] } ;
set Lk = { k where k is Element of : S1[k] } ;
A2:
rng p = { c where c is Element of : S2[c] } /\ { k where k is Element of : S1[k] }
by A1, Th45;
{ c where c is Element of : S2[c] } is Subset of
from DOMAIN_1:sch 7();
hence
{ c where c is Element of : S2[c] } is non empty Subset of
by A2; { k where k is Element of : p . k <= k } is non empty Subset of
{ k where k is Element of : S1[k] } is Subset of
from DOMAIN_1:sch 7();
hence
{ k where k is Element of : p . k <= k } is non empty Subset of
by A2; verum