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 q in A "/\" B ; :: thesis: ex b being Element of L st
( b in A & q <= b )
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 & q <= x )
thus x in A by A2; :: thesis: q <= x
thus q <= x by A1, YELLOW_0:23; :: thesis: verum