let L be non empty reflexive antisymmetric complete RelStr ; :: thesis: for D being Subset of L
for x being Element of L st x in D holds
(sup D) "/\" x = x
let D be Subset of L; :: thesis: for x being Element of L st x in D holds
(sup D) "/\" x = x
let x be Element of L; :: thesis: ( x in D implies (sup D) "/\" x = x )
assume A1: x in D ; :: thesis: (sup D) "/\" x = x
D is_<=_than sup D by YELLOW_0:32;
then x <= sup D by A1, LATTICE3:def 9;
hence (sup D) "/\" x = x by YELLOW_0:25; :: thesis: verum