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 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;
assume A7: 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 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