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 )
set b = the Element of B;
take q "\/" the Element of B ; :: thesis: ( q "\/" the Element of B in A "\/" B & q <= q "\/" the Element of B )
thus q "\/" the Element of B in A "\/" B by A1; :: thesis: q <= q "\/" the Element of B
thus q <= q "\/" the Element of B by YELLOW_0:22; :: thesis: verum