let L be antisymmetric with_suprema RelStr ; :: thesis: for X being lower Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
let X be lower Subset of L; :: thesis: ( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
thus ( X is directed implies for x, y being Element of L st x in X & y in X holds
x "\/" y in X ) :: thesis: ( ( for x, y being Element of L st x in X & y in X holds
x "\/" y in X ) implies X is directed )

proof

assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: for x, y being Element of L st x in X & y in X holds
x "\/" y in X
let x, y be Element of L; :: thesis: ( x in X & y in X implies x "\/" y in X )
assume ( x in X & y in X ) ; :: thesis: x "\/" y in X
then consider z being Element of L such that
A2: ( z in X & x <= z & y <= z ) by A1;
x "\/" y <= z by A2, YELLOW_0:22;
hence x "\/" y in X by A2, Def19; :: thesis: verum

end;

assume A3: for x, y being Element of L st x in X & y in X holds
x "\/" y in X ; :: thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
then ( x "\/" y in X & x <= x "\/" y & y <= x "\/" y ) by A3, YELLOW_0:22;
hence ex z being Element of L st
( z in X & x <= z & y <= z ) ; :: thesis: verum