let L be antisymmetric with_suprema RelStr ; :: thesis: for A, B being Subset of holds A "\/" B is_coarser_than A
let A, B be Subset of ; :: thesis: A "\/" B is_coarser_than A
let q be Element of ; :: according to YELLOW_4:def 2 :: thesis: ( q in A "\/" B implies ex a being Element of st
( a in A & a <= q ) )
assume q in A "\/" B ; :: thesis: ex a being Element of st
( a in A & a <= q )
then consider x, y being Element of 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