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 ) :: 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 )

proof

assume A1: S is meet-closed ; :: thesis: for x, y being Element of L st x in S & y in S holds
inf {x,y} in S
let x, y be Element of L; :: thesis: ( x in S & y in S implies inf {x,y} in S )
assume that
A2: x in S and
A3: y in S ; :: thesis: inf {x,y} in S
ex_inf_of {x,y},L by YELLOW_0:21;
hence inf {x,y} in S by A1, A2, A3, Th15; :: thesis: verum

end;

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