let X be set ; :: thesis: for Y being upper Subset of (BoolePoset X) holds
( Y is filtered iff for x, y being set st x in Y & y in Y holds
x /\ y in Y )
let Y be upper Subset of (BoolePoset X); :: thesis: ( Y is filtered iff for x, y being set st x in Y & y in Y holds
x /\ y in Y )

hereby :: thesis: ( ( for x, y being set st x in Y & y in Y holds
x /\ y in Y ) implies Y is filtered )

assume A1: Y is filtered ; :: thesis: for x, y being set st x in Y & y in Y holds
x /\ y in Y
let x, y be set ; :: thesis: ( x in Y & y in Y implies x /\ y in Y )
assume A2: ( x in Y & y in Y ) ; :: thesis: x /\ y in Y
then reconsider a = x, b = y as Element of (BoolePoset X) ;
a "/\" b in Y by A1, A2, WAYBEL_0:41;
hence x /\ y in Y by YELLOW_1:17; :: thesis: verum

end;

assume A3: for x, y being set st x in Y & y in Y holds
x /\ y in Y ; :: thesis: Y is filtered

now :: thesis: for a, b being Element of (BoolePoset X) st a in Y & b in Y holds
a "/\" b in Y

let a, b be Element of (BoolePoset X); :: thesis: ( a in Y & b in Y implies a "/\" b in Y )
assume ( a in Y & b in Y ) ; :: thesis: a "/\" b in Y
then a /\ b in Y by A3;
hence a "/\" b in Y by YELLOW_1:17; :: thesis: verum

end;

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