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