let L be non empty Poset; :: thesis: for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
let p be Function of L,L; :: thesis: ( p is projection implies for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure )
assume that
A1: p is idempotent and
A2: p is monotone ; :: according to WAYBEL_1:def 13 :: thesis: for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
let Lc be non empty Subset of L; :: thesis: ( Lc = { c where c is Element of L : c <= p . c } implies for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure )
assume A3: Lc = { c where c is Element of L : c <= p . c } ; :: thesis: for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
let pc be Function of (subrelstr Lc),(subrelstr Lc); :: thesis: ( pc = p | Lc implies pc is closure )
assume A4: pc = p | Lc ; :: thesis: pc is closure
A5: dom pc = the carrier of (subrelstr Lc) by FUNCT_2:def 1;

hereby :: according to QUANTAL1:def 9,WAYBEL_1:def 13,WAYBEL_1:def 14 :: thesis: id (subrelstr Lc) <= pc

now :: thesis: for x being Element of (subrelstr Lc) holds (pc * pc) . x = pc . x

let x be Element of (subrelstr Lc); :: thesis: (pc * pc) . x = pc . x
A6: x is Element of L by YELLOW_0:58;
A7: pc . x = p . x by A4, A5, FUNCT_1:47;
then p . (p . x) = pc . (pc . x) by A4, A5, FUNCT_1:47
.= (pc * pc) . x by A5, FUNCT_1:13 ;
hence (pc * pc) . x = pc . x by A1, A7, A6, YELLOW_2:18; :: thesis: verum

end;

hence pc * pc = pc by FUNCT_2:63; :: thesis: pc is monotone
thus pc is monotone :: thesis: verum

proof

let x1, x2 be Element of (subrelstr Lc); :: according to WAYBEL_1:def 2 :: thesis: ( x1 <= x2 implies pc . x1 <= pc . x2 )
reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
assume x1 <= x2 ; :: thesis: pc . x1 <= pc . x2
then x19 <= x29 by YELLOW_0:59;
then A8: p . x19 <= p . x29 by A2;
( pc . x1 = p . x19 & pc . x2 = p . x29 ) by A4, A5, FUNCT_1:47;
hence pc . x1 <= pc . x2 by A8, YELLOW_0:60; :: thesis: verum

end;

end;

now :: thesis: for x being Element of (subrelstr Lc) holds (id (subrelstr Lc)) . x <= pc . x

let x be Element of (subrelstr Lc); :: thesis: (id (subrelstr Lc)) . x <= pc . x
reconsider x9 = x as Element of L by YELLOW_0:58;
x in the carrier of (subrelstr Lc) ;
then x in Lc by YELLOW_0:def 15;
then A9: ex c being Element of L st
( x = c & c <= p . c ) by A3;
pc . x = p . x9 by A4, A5, FUNCT_1:47;
then x <= pc . x by A9, YELLOW_0:60;
hence (id (subrelstr Lc)) . x <= pc . x ; :: thesis: verum

end;

hence id (subrelstr Lc) <= pc by YELLOW_2:9; :: thesis: verum