let L be antisymmetric with_suprema RelStr ; :: thesis: for D being Subset of L
for x being Element of L holds x is_<=_than {x} "\/" D
let D be Subset of L; :: thesis: for x being Element of L holds x is_<=_than {x} "\/" D
let x be Element of L; :: thesis: x is_<=_than {x} "\/" D
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in {x} "\/" D or x <= b )
A1: {x} "\/" D = { (x "\/" h) where h is Element of L : h in D } by Th15;
assume b in {x} "\/" D ; :: thesis: x <= b
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 10;
hence x <= b by A2, LATTICE3:def 13; :: thesis: verum