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 A5: ex l being Element of L st
( 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