let X be set ; :: thesis: for Y being non empty lower Subset of (BoolePoset X) holds
( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y )
let Y be non empty lower Subset of (BoolePoset X); :: thesis: ( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y )
hereby :: thesis: ( ( for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y ) implies Y is directed )
assume A1: Y is directed ; :: thesis: for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y
let Z be finite Subset-Family of X; :: thesis: ( Z c= Y implies union Z in Y )
reconsider B = Z as Subset of (BoolePoset X) by Th2;
assume Z c= Y ; :: thesis: union Z in Y
then reconsider A = Z as finite Subset of Y ;
A2: ( A <> {} implies sup B in Y ) by A1, WAYBEL_0:42;
Bottom (BoolePoset X) in Y by A1, WAYBEL_4:21;
hence union Z in Y by A2, YELLOW_1:18, YELLOW_1:21, ZFMISC_1:2; :: thesis: verum
end;
assume A3: for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y ; :: thesis: Y is directed
A4: the carrier of (BoolePoset X) = bool X by Th2;
now :: thesis: for A being finite Subset of Y st A <> {} holds
"\/" (A,(BoolePoset X)) in Y
let A be finite Subset of Y; :: thesis: ( A <> {} implies "\/" (A,(BoolePoset X)) in Y )
reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1:1;
assume A <> {} ; :: thesis: "\/" (A,(BoolePoset X)) in Y
reconsider Z = Z as finite Subset-Family of X ;
A c= the carrier of (BoolePoset X) by XBOOLE_1:1;
then union Z = "\/" (A,(BoolePoset X)) by YELLOW_1:21;
hence "\/" (A,(BoolePoset X)) in Y by A3; :: thesis: verum
end;
hence Y is directed by WAYBEL_0:42; :: thesis: verum