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

proof

let x be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not x in X or p . ("/\" X,L) <= x )
assume A4: x in X ; :: thesis: p . ("/\" X,L) <= x
then x in the carrier of (subrelstr Lk) ;
then x in Lk 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:31;
then x >= "/\" X,L by A4, LATTICE3:def 8;
then p . x >= p . ("/\" X,L) by A1, Def2;
hence p . ("/\" X,L) <= x by A5, ORDERS_2:26; :: thesis: verum

end;

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