let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for V being Subset of L

for x, y being Element of L st x <= y holds

{x} "\/" V is_finer_than {y} "\/" V

let V be Subset of L; :: thesis: for x, y being Element of L st x <= y holds

{x} "\/" V is_finer_than {y} "\/" V

let x, y be Element of L; :: thesis: ( x <= y implies {x} "\/" V is_finer_than {y} "\/" V )

assume A1: x <= y ; :: thesis: {x} "\/" V is_finer_than {y} "\/" V

A2: {x} "\/" V = { (x "\/" s) where s is Element of L : s in V } by YELLOW_4:15;

let b be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( not b in {x} "\/" V or ex b_{1} being Element of the carrier of L st

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

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

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

then consider s being Element of L such that

A3: b = x "\/" s and

A4: s in V by A2;

take a = y "\/" s; :: thesis: ( a in {y} "\/" V & b <= a )

{y} "\/" V = { (y "\/" t) where t is Element of L : t in V } by YELLOW_4:15;

hence a in {y} "\/" V by A4; :: thesis: b <= a

thus b <= a by A1, A3, WAYBEL_1:2; :: thesis: verum

for x, y being Element of L st x <= y holds

{x} "\/" V is_finer_than {y} "\/" V

let V be Subset of L; :: thesis: for x, y being Element of L st x <= y holds

{x} "\/" V is_finer_than {y} "\/" V

let x, y be Element of L; :: thesis: ( x <= y implies {x} "\/" V is_finer_than {y} "\/" V )

assume A1: x <= y ; :: thesis: {x} "\/" V is_finer_than {y} "\/" V

A2: {x} "\/" V = { (x "\/" s) where s is Element of L : s in V } by YELLOW_4:15;

let b be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( not b in {x} "\/" V or ex b

( b

assume b in {x} "\/" V ; :: thesis: ex b

( b

then consider s being Element of L such that

A3: b = x "\/" s and

A4: s in V by A2;

take a = y "\/" s; :: thesis: ( a in {y} "\/" V & b <= a )

{y} "\/" V = { (y "\/" t) where t is Element of L : t in V } by YELLOW_4:15;

hence a in {y} "\/" V by A4; :: thesis: b <= a

thus b <= a by A1, A3, WAYBEL_1:2; :: thesis: verum