let L be non empty antisymmetric complete RelStr ; :: thesis: for X being upper Subset of L st inf X in X holds
X = uparrow (inf X)
let X be upper Subset of L; :: thesis: ( inf X in X implies X = uparrow (inf X) )
assume A1: inf X in X ; :: thesis: X = uparrow (inf X)
X is_>=_than inf X by YELLOW_0:33;
hence X c= uparrow (inf X) by YELLOW_2:2; :: according to XBOOLE_0:def 10 :: thesis: uparrow (inf X) c= X
thus uparrow (inf X) c= X by A1, WAYBEL11:42; :: thesis: verum