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 9 :: thesis: ( not q in A "/\" B or q <= a "/\" b )
assume q in A "/\" B ; :: thesis: q <= a "/\" b
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 q <= a "/\" b by A2, YELLOW_3:2; :: thesis: verum