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: {y} "/\" V is_coarser_than {x} "/\" V
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 b₁ being Element of the carrier of L st
( b₁ in {x} "/\" V & b₁ <= b ) )
assume b in {y} "/\" V ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in {x} "/\" V & b₁ <= 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 A1, A3, WAYBEL_1:1; :: thesis: verum