let L be antisymmetric with_suprema RelStr ; :: thesis: for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S holds
sup {x,y} in S )
let S be Subset of L; :: thesis: ( S is join-closed iff for x, y being Element of L st x in S & y in S holds
sup {x,y} in S )
thus ( S is join-closed implies for x, y being Element of L st x in S & y in S holds
sup {x,y} in S ) by YELLOW_0:20, Th16; :: thesis: ( ( for x, y being Element of L st x in S & y in S holds
sup {x,y} in S ) implies S is join-closed )
assume for x, y being Element of L st x in S & y in S holds
sup {x,y} in S ; :: thesis: S is join-closed
then for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ;
hence S is join-closed by Th16; :: thesis: verum