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 A5: ex l being Element of L st
( x = l & l >= p . l ) by A2;
"/\" (X,L) is_<=_than X by A3, YELLOW_0:31;
then x >= "/\" (X,L) by A4;
then p . x >= p . ("/\" (X,L)) by A1;
hence p . ("/\" (X,L)) <= x by A5, ORDERS_2:3; :: 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