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