let X be set ; :: thesis: for Y being non empty upper Subset of (BoolePoset X) holds
( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y )
let Y be non empty upper Subset of (BoolePoset X); :: thesis: ( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y )

hereby :: thesis: ( ( for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y ) implies Y is filtered )

assume A1: Y is filtered ; :: thesis: for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y
then Top (BoolePoset X) in Y by WAYBEL_4:22;
then A2: X in Y by YELLOW_1:19;
let Z be finite Subset-Family of X; :: thesis: ( Z c= Y implies Intersect Z in Y )
reconsider B = Z as Subset of (BoolePoset X) by Th2;
assume Z c= Y ; :: thesis: Intersect Z in Y
then reconsider A = Z as finite Subset of Y ;
( A <> {} implies ( inf B in Y & inf B = meet B ) ) by A1, WAYBEL_0:43, YELLOW_1:20;
hence Intersect Z in Y by A2, SETFAM_1:def 9; :: thesis: verum

end;

assume A3: for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y ; :: thesis: Y is filtered
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 A5: 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 "/\" (A,(BoolePoset X)) = meet Z by A5, YELLOW_1:20
.= Intersect Z by A5, SETFAM_1:def 9 ;
hence "/\" (A,(BoolePoset X)) in Y by A3; :: thesis: verum

end;

hence Y is filtered by WAYBEL_0:43; :: thesis: verum