let L be antisymmetric with_suprema RelStr ; :: thesis: for A being Subset of L
for B being non empty Subset of L holds A is_finer_than A "\/" B
let A be Subset of L; :: thesis: for B being non empty Subset of L holds A is_finer_than A "\/" B
let B be non empty Subset of L; :: thesis: A is_finer_than A "\/" B
let q be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( q in A implies ex b being Element of L st
( b in A "\/" B & q <= b ) )
assume A1: q in A ; :: thesis: ex b being Element of L st
( b in A "\/" B & q <= b )
consider b being Element of B;
take q "\/" b ; :: thesis: ( q "\/" b in A "\/" B & q <= q "\/" b )
thus q "\/" b in A "\/" B by A1; :: thesis: q <= q "\/" b
thus q <= q "\/" b by YELLOW_0:22; :: thesis: verum