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 A2: q in A "/\" B ; :: thesis: q <= a "/\" b
consider x, y being Element of L such that
A3: ( q = x "/\" y & x in A & y in B ) by A2;
( a >= x & b >= y ) by A1, A3, LATTICE3:def 9;
hence q <= a "/\" b by A3, YELLOW_3:2; :: thesis: verum