let L be transitive antisymmetric with_infima RelStr ; :: thesis: for a, b being Element of L
for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "/\" b is_<=_than A "/\" B
let a, b be Element of L; :: thesis: for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "/\" b is_<=_than A "/\" B
let A, B be Subset of L; :: thesis: ( a is_<=_than A & b is_<=_than B implies a "/\" b is_<=_than A "/\" B )
assume A1: ( a is_<=_than A & b is_<=_than B ) ; :: thesis: a "/\" b is_<=_than A "/\" B
let q be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not q in A "/\" B or a "/\" b <= q )
assume q in A "/\" B ; :: thesis: a "/\" b <= q
then consider x, y being Element of L such that
A2: q = x "/\" y and
A3: ( x in A & y in B ) ;
( a <= x & b <= y ) by A1, A3;
hence a "/\" b <= q by A2, YELLOW_3:2; :: thesis: verum