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_{1} being Element of the carrier of L st

( b_{1} in {x} "/\" V & b_{1} <= b ) )

assume b in {y} "/\" V ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in {x} "/\" V & b_{1} <= 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

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

( b

assume b in {y} "/\" V ; :: thesis: ex 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