let L be non empty reflexive antisymmetric complete RelStr ; :: thesis: for D being Subset of
for x being Element of st x in D holds
(inf D) "\/" x = x
let D be Subset of ; :: thesis: for x being Element of st x in D holds
(inf D) "\/" x = x
let x be Element of ; :: 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