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 q in A "\/" B ; :: thesis: ex a being Element of L st
( a in A & a <= q )
then consider x, y being Element of L such that
A1: q = x "\/" y and
A2: x in A and
y in B ;
take x ; :: thesis: ( x in A & x <= q )
thus x in A by A2; :: thesis: x <= q
thus x <= q by A1, YELLOW_0:22; :: thesis: verum