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 )

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 that

A8: x in X and

A9: y in X ; :: thesis: ex z being Element of L st

( z in X & x <= z & y <= z )

A10: x <= x "\/" y by YELLOW_0:22;

y <= x "\/" y by YELLOW_0:22;

hence ex z being Element of L st

( z in X & x <= z & y <= z ) by A7, A8, A9, A10; :: thesis: verum

( 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 A7:
for x, y being Element of L st x in X & y in X holds
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 that

A2: x in X and

A3: y in X ; :: thesis: x "\/" y in X

consider z being Element of L such that

A4: z in X and

A5: x <= z and

A6: y <= z by A1, A2, A3;

x "\/" y <= z by A5, A6, YELLOW_0:22;

hence x "\/" y in X by A4, Def19; :: thesis: verum

end;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 that

A2: x in X and

A3: y in X ; :: thesis: x "\/" y in X

consider z being Element of L such that

A4: z in X and

A5: x <= z and

A6: y <= z by A1, A2, A3;

x "\/" y <= z by A5, A6, YELLOW_0:22;

hence x "\/" y in X by A4, Def19; :: thesis: verum

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 that

A8: x in X and

A9: y in X ; :: thesis: ex z being Element of L st

( z in X & x <= z & y <= z )

A10: x <= x "\/" y by YELLOW_0:22;

y <= x "\/" y by YELLOW_0:22;

hence ex z being Element of L st

( z in X & x <= z & y <= z ) by A7, A8, A9, A10; :: thesis: verum