let L be antisymmetric with_suprema RelStr ; :: thesis: for A, B being Subset of L holds A "\/" B is_coarser_than A
let A, B be Subset of L; :: thesis: A "\/" B is_coarser_than A
let q be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( q in A "\/" B implies ex a being Element of L st
( a in A & a <= q ) )
assume A1: q in A "\/" B ; :: thesis: ex a being Element of L st
( a in A & a <= q )
consider x, y being Element of L such that
A2: ( q = x "\/" y & x in A & y in B ) by A1;
take x ; :: thesis: ( x in A & x <= q )
thus x in A by A2; :: thesis: x <= q
thus x <= q by A2, YELLOW_0:22; :: thesis: verum