let L be with_suprema Poset; :: thesis: for X being non empty lower Subset of L holds

( X is directed iff for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X )

let X be non empty lower Subset of L; :: thesis: ( X is directed iff for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X )

thus ( X is directed implies for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X ) :: thesis: ( ( for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X ) implies X is directed )

"\/" (Y,L) in X ; :: thesis: X is directed

set x = the Element of X;

reconsider x = the Element of X as Element of L ;

( X is directed iff for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X )

let X be non empty lower Subset of L; :: thesis: ( X is directed iff for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X )

thus ( X is directed implies for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X ) :: thesis: ( ( for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X ) implies X is directed )

proof

assume A5:
for Y being finite Subset of X st Y <> {} holds
assume A1:
X is directed
; :: thesis: for Y being finite Subset of X st Y <> {} holds

"\/" (Y,L) in X

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "\/" (Y,L) in X )

assume A2: Y <> {} ; :: thesis: "\/" (Y,L) in X

consider z being Element of L such that

A3: z in X and

A4: Y is_<=_than z by A1, Th1;

Y c= the carrier of L by XBOOLE_1:1;

then ex_sup_of Y,L by A2, YELLOW_0:54;

then "\/" (Y,L) <= z by A4, YELLOW_0:30;

hence "\/" (Y,L) in X by A3, Def19; :: thesis: verum

end;"\/" (Y,L) in X

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "\/" (Y,L) in X )

assume A2: Y <> {} ; :: thesis: "\/" (Y,L) in X

consider z being Element of L such that

A3: z in X and

A4: Y is_<=_than z by A1, Th1;

Y c= the carrier of L by XBOOLE_1:1;

then ex_sup_of Y,L by A2, YELLOW_0:54;

then "\/" (Y,L) <= z by A4, YELLOW_0:30;

hence "\/" (Y,L) in X by A3, Def19; :: thesis: verum

"\/" (Y,L) in X ; :: thesis: X is directed

set x = the Element of X;

reconsider x = the Element of X as Element of L ;

now :: thesis: for Y being finite Subset of X ex x being Element of L st

( x in X & x is_>=_than Y )

hence
X is directed
by Th1; :: thesis: verum( x in X & x is_>=_than Y )

let Y be finite Subset of X; :: thesis: ex x being Element of L st

( b_{2} in X & b_{2} is_>=_than x )

end;( b

per cases
( Y = {} or Y <> {} )
;

end;

suppose
Y = {}
; :: thesis: ex x being Element of L st

( b_{2} in X & b_{2} is_>=_than x )

( b

then
x is_>=_than Y
;

hence ex x being Element of L st

( x in X & x is_>=_than Y ) ; :: thesis: verum

end;hence ex x being Element of L st

( x in X & x is_>=_than Y ) ; :: thesis: verum

suppose A6:
Y <> {}
; :: thesis: ex x being Element of L st

( b_{2} in X & b_{2} is_>=_than x )

( b

Y c= the carrier of L
by XBOOLE_1:1;

then ex_sup_of Y,L by A6, YELLOW_0:54;

then "\/" (Y,L) is_>=_than Y by YELLOW_0:30;

hence ex x being Element of L st

( x in X & x is_>=_than Y ) by A5, A6; :: thesis: verum

end;then ex_sup_of Y,L by A6, YELLOW_0:54;

then "\/" (Y,L) is_>=_than Y by YELLOW_0:30;

hence ex x being Element of L st

( x in X & x is_>=_than Y ) by A5, A6; :: thesis: verum