let L be transitive antisymmetric with_infima RelStr ; :: thesis: for V being Subset of L
for x, y being Element of L st x <= y holds
{y} "/\" V is_coarser_than {x} "/\" V

let V be Subset of L; :: thesis: for x, y being Element of L st x <= y holds
{y} "/\" V is_coarser_than {x} "/\" V

let x, y be Element of L; :: thesis: ( x <= y implies {y} "/\" V is_coarser_than {x} "/\" V )
assume A1: x <= y ; :: thesis:
A2: {y} "/\" V = { (y "/\" s) where s is Element of L : s in V } by YELLOW_4:42;
let b be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not b in {y} "/\" V or ex b1 being Element of the carrier of L st
( b1 in {x} "/\" V & b1 <= b ) )

assume b in {y} "/\" V ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in {x} "/\" V & b1 <= b )

then consider s being Element of L such that
A3: b = y "/\" s and
A4: s in V by A2;
take a = x "/\" s; :: thesis: ( a in {x} "/\" V & a <= b )
{x} "/\" V = { (x "/\" t) where t is Element of L : t in V } by YELLOW_4:42;
hence a in {x} "/\" V by A4; :: thesis: a <= b
thus a <= b by ; :: thesis: verum