let X be non empty set ; :: thesis:
let FF be non empty Subset-Family of X; :: thesis:
assume A1: FF is Filter of (BooleLatt X) ; :: thesis:

now :: thesis:

set Z = LattPOSet (BooleLatt X);
reconsider FF = FF as Subset of (LattPOSet (BooleLatt X)) by A1;
A2: FF is filtered

proof

for x, y being Element of (LattPOSet (BooleLatt X)) st x in FF & y in FF holds
ex z being Element of (LattPOSet (BooleLatt X)) st
( z in FF & z <= x & z <= y )

proof

let x, y be Element of (LattPOSet (BooleLatt X)); :: thesis:
assume A3: ( x in FF & y in FF ) ; :: thesis:
reconsider x1 = x, y1 = y as Element of (BooleLatt X) ;
set z = x1 "/\" y1;

A4: now :: thesis:

( x1 /\ y1 c= x1 & x1 /\ y1 c= y1 ) by XBOOLE_1:17;
hence ( (x1 "/\" y1) % <= x1 % & (x1 "/\" y1) % <= y1 % ) by LATTICE3:2, LATTICE3:7; :: thesis:

end;

x /\ y in FF by A1, A3, Th31;
hence ex z being Element of (LattPOSet (BooleLatt X)) st
( z in FF & z <= x & z <= y ) by A4; :: thesis:

end;

hence FF is filtered ; :: thesis:

end;

FF is upper

proof

for x, y being Element of (LattPOSet (BooleLatt X)) st x in FF & x <= y holds
y in FF

proof

let x, y be Element of (LattPOSet (BooleLatt X)); :: thesis:
assume A5: ( x in FF & x <= y ) ; :: thesis:
reconsider x = x, y = y as Element of (BooleLatt X) ;
A6: x % <= y % by A5;
( x in FF & x c= y ) by A5, A6, LATTICE3:2, LATTICE3:7;
hence y in FF by A1, Th31; :: thesis:

end;

hence FF is upper ; :: thesis:

end;

hence FF is Filter of (BoolePoset X) by A2; :: thesis:

end;

hence FF is Filter of (BoolePoset X) ; :: thesis: