let L be non empty transitive antisymmetric complete RelStr ; :: thesis: for A being Subset of L
for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)
let A be Subset of L; :: thesis: for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)
let B be non empty Subset of L; :: thesis: A is_>=_than inf (A "/\" B)
ex_inf_of A "/\" B,L by YELLOW_0:17;
then A1: A "/\" B is_>=_than inf (A "/\" B) by YELLOW_0:def 10;
let x be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not x in A or inf (A "/\" B) <= x )
assume A2: x in A ; :: thesis: inf (A "/\" B) <= x
consider b being Element of B;
x "/\" b in A "/\" B by A2;
then A3: x "/\" b >= inf (A "/\" B) by A1, LATTICE3:def 8;
ex xx being Element of L st
( x >= xx & b >= xx & ( for c being Element of L st x >= c & b >= c holds
xx >= c ) ) by LATTICE3:def 11;
then x >= x "/\" b by LATTICE3:def 14;
hence inf (A "/\" B) <= x by A3, YELLOW_0:def 2; :: thesis: verum