let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for D being Subset of L
for x being Element of L st x is_>=_than D holds
{x} "/\" D = D
let D be Subset of L; :: thesis: for x being Element of L st x is_>=_than D holds
{x} "/\" D = D
let x be Element of L; :: thesis: ( x is_>=_than D implies {x} "/\" D = D )
assume A1: x is_>=_than D ; :: thesis: {x} "/\" D = D
A2: {x} "/\" D = { (x "/\" y) where y is Element of L : y in D } by Th42;
thus {x} "/\" D c= D :: according to XBOOLE_0:def 10 :: thesis: D c= {x} "/\" D

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {x} "/\" D or q in D )
assume q in {x} "/\" D ; :: thesis: q in D
then consider y being Element of L such that
A3: ( q = x "/\" y & y in D ) by A2;
x >= y by A1, A3, LATTICE3:def 9;
hence q in D by A3, YELLOW_0:25; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in D or q in {x} "/\" D )
assume A4: q in D ; :: thesis: q in {x} "/\" D
then reconsider D1 = D as non empty Subset of L ;
reconsider y = q as Element of D1 by A4;
x >= y by A1, LATTICE3:def 9;
then q = x "/\" y by YELLOW_0:25;
hence q in {x} "/\" D by A2; :: thesis: verum