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 object ; :: 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 and
A4: y in D by A2;
x >= y by A1, A4;
hence q in D by A3, A4, YELLOW_0:25; :: thesis: verum
end;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D or q in {x} "/\" D )
assume A5: 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 A5;
x >= y by A1;
then q = x "/\" y by YELLOW_0:25;
hence q in {x} "/\" D by A2; :: thesis: verum