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)
set b = the Element of B;
let x be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not x in A or inf (A "/\" B) <= x )
assume x in A ; :: thesis: inf (A "/\" B) <= x
then A1: x "/\" the Element of B in A "/\" B ;
ex xx being Element of L st
( x >= xx & the Element of B >= xx & ( for c being Element of L st x >= c & the Element of B >= c holds
xx >= c ) ) by LATTICE3:def 11;
then A2: x >= x "/\" the Element of B by LATTICE3:def 14;
ex_inf_of A "/\" B,L by YELLOW_0:17;
then A "/\" B is_>=_than inf (A "/\" B) by YELLOW_0:def 10;
then x "/\" the Element of B >= inf (A "/\" B) by A1;
hence inf (A "/\" B) <= x by A2, YELLOW_0:def 2; :: thesis: verum