let L be antisymmetric with_infima RelStr ; :: thesis: for A, B being Subset of L holds A "/\" B is_finer_than A
let A, B be Subset of L; :: thesis: A "/\" B is_finer_than A
let q be Element of L; :: according to YELLOW_4:def 1 :: thesis: ( q in A "/\" B implies ex b being Element of L st
( b in A & q <= b ) )
assume A1: q in A "/\" B ; :: thesis: ex b being Element of L st
( b in A & q <= b )
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 & q <= x )
thus x in A by A2; :: thesis: q <= x
thus q <= x by A2, YELLOW_0:23; :: thesis: verum