let L be non empty antisymmetric complete RelStr ; :: thesis: for X being lower Subset of L st sup X in X holds
X = downarrow (sup X)
let X be lower Subset of L; :: thesis: ( sup X in X implies X = downarrow (sup X) )
assume A1: sup X in X ; :: thesis: X = downarrow (sup X)
X is_<=_than sup X by YELLOW_0:32;
hence X c= downarrow (sup X) by YELLOW_2:1; :: according to XBOOLE_0:def 10 :: thesis: downarrow (sup X) c= X
thus downarrow (sup X) c= X by A1, WAYBEL11:6; :: thesis: verum