let L be antisymmetric with_infima RelStr ; :: thesis: for S being Subset of L holds

( S is meet-closed iff for x, y being Element of L st x in S & y in S holds

inf {x,y} in S )

let S be Subset of L; :: thesis: ( S is meet-closed iff for x, y being Element of L st x in S & y in S holds

inf {x,y} in S )

thus ( S is meet-closed implies for x, y being Element of L st x in S & y in S holds

inf {x,y} in S ) by YELLOW_0:21, Th15; :: thesis: ( ( for x, y being Element of L st x in S & y in S holds

inf {x,y} in S ) implies S is meet-closed )

assume for x, y being Element of L st x in S & y in S holds

inf {x,y} in S ; :: thesis: S is meet-closed

then for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S ;

hence S is meet-closed by Th15; :: thesis: verum

( S is meet-closed iff for x, y being Element of L st x in S & y in S holds

inf {x,y} in S )

let S be Subset of L; :: thesis: ( S is meet-closed iff for x, y being Element of L st x in S & y in S holds

inf {x,y} in S )

thus ( S is meet-closed implies for x, y being Element of L st x in S & y in S holds

inf {x,y} in S ) by YELLOW_0:21, Th15; :: thesis: ( ( for x, y being Element of L st x in S & y in S holds

inf {x,y} in S ) implies S is meet-closed )

assume for x, y being Element of L st x in S & y in S holds

inf {x,y} in S ; :: thesis: S is meet-closed

then for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S ;

hence S is meet-closed by Th15; :: thesis: verum