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