let L be non empty Poset; :: thesis: for p being Function of L,L st p is monotone holds
for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting
let p be Function of L,L; :: thesis: ( p is monotone implies for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting )
assume A1: p is monotone ; :: thesis: for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting
let Lc be Subset of L; :: thesis: ( Lc = { c where c is Element of L : c <= p . c } implies subrelstr Lc is sups-inheriting )
assume A2: Lc = { c where c is Element of L : c <= p . c } ; :: thesis: subrelstr Lc is sups-inheriting
let X be Subset of (subrelstr Lc); :: according to YELLOW_0:def 19 :: thesis: ( not ex_sup_of X,L or "\/" X,L in the carrier of (subrelstr Lc) )
assume A3: ex_sup_of X,L ; :: thesis: "\/" X,L in the carrier of (subrelstr Lc)
p . ("\/" X,L) is_>=_than X

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= p . ("\/" X,L) )
assume A4: x in X ; :: thesis: x <= p . ("\/" X,L)
then x in the carrier of (subrelstr Lc) ;
then x in Lc by YELLOW_0:def 15;
then consider l being Element of L such that
A5: ( x = l & l <= p . l ) by A2;
"\/" X,L is_>=_than X by A3, YELLOW_0:30;
then x <= "\/" X,L by A4, LATTICE3:def 9;
then p . x <= p . ("\/" X,L) by A1, Def2;
hence x <= p . ("\/" X,L) by A5, ORDERS_2:26; :: thesis: verum

end;

then "\/" X,L <= p . ("\/" X,L) by A3, YELLOW_0:30;
then "\/" X,L in Lc by A2;
hence "\/" X,L in the carrier of (subrelstr Lc) by YELLOW_0:def 15; :: thesis: verum