let L be antisymmetric with_infima RelStr ; :: thesis: for A being Subset of L
for B being non empty Subset of L holds A is_coarser_than A "/\" B
let A be Subset of L; :: thesis: for B being non empty Subset of L holds A is_coarser_than A "/\" B
let B be non empty Subset of L; :: thesis: A is_coarser_than A "/\" B
consider b being object such that
A1: b in B by XBOOLE_0:def 1;
reconsider b = b as Element of B by A1;
let q be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( q in A implies ex a being Element of L st
( a in A "/\" B & a <= q ) )
assume A2: q in A ; :: thesis: ex a being Element of L st
( a in A "/\" B & a <= q )
take q "/\" b ; :: thesis: ( q "/\" b in A "/\" B & q "/\" b <= q )
thus q "/\" b in A "/\" B by A2; :: thesis: q "/\" b <= q
thus q "/\" b <= q by YELLOW_0:23; :: thesis: verum