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 )
proof
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;
assume A5: for Y being finite Subset of X st Y <> {} holds
"\/" (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 )
let Y be finite Subset of X; :: thesis: ex x being Element of L st
( b2 in X & b2 is_>=_than x )
per cases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; :: thesis: ex x being Element of L st
( b2 in X & b2 is_>=_than x )
then x is_>=_than Y ;
hence ex x being Element of L st
( x in X & x is_>=_than Y ) ; :: thesis: verum
end;
suppose A6: Y <> {} ; :: thesis: ex x being Element of L st
( b2 in X & b2 is_>=_than x )
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;
end;
end;
hence X is directed by Th1; :: thesis: verum