let L be antisymmetric with_infima RelStr ; :: thesis: for D being Subset of L
for x being Element of L holds {x} "/\" D is_<=_than x
let D be Subset of L; :: thesis: for x being Element of L holds {x} "/\" D is_<=_than x
let x be Element of L; :: thesis: {x} "/\" D is_<=_than x
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in {x} "/\" D or b <= x )
A1: {x} "/\" D = { (x "/\" h) where h is Element of L : h in D } by Th42;
assume b in {x} "/\" D ; :: thesis: b <= x
then consider h being Element of L such that
A2: b = x "/\" h and
h in D by A1;
ex w being Element of L st
( x >= w & h >= w & ( for c being Element of L st x >= c & h >= c holds
w >= c ) ) by LATTICE3:def 11;
hence b <= x by A2, LATTICE3:def 14; :: thesis: verum