let L be reflexive antisymmetric with_suprema 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 Th15;
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:24; :: 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:24;
hence q in {x} "\/" D by A2; :: thesis: verum