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
(inf D) "\/" x = x
let D be Subset of L; :: thesis: for x being Element of L st x in D holds
(inf D) "\/" x = x
let x be Element of L; :: thesis: ( x in D implies (inf D) "\/" x = x )
assume A1: x in D ; :: thesis: (inf D) "\/" x = x
D is_>=_than inf D by YELLOW_0:33;
then inf D <= x by A1, LATTICE3:def 8;
hence (inf D) "\/" x = x by YELLOW_0:24; :: thesis: verum