let X be non empty set ; :: thesis: for FF being non empty Subset-Family of X st FF is Filter of (BooleLatt X) holds
FF is Filter of (BoolePoset X)
let FF be non empty Subset-Family of X; :: thesis: ( FF is Filter of (BooleLatt X) implies FF is Filter of (BoolePoset X) )
assume A1: FF is Filter of (BooleLatt X) ; :: thesis: FF is Filter of (BoolePoset X)

now :: thesis: FF is Filter of (BoolePoset X)

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: ( x in FF & y in FF implies ex z being Element of (LattPOSet (BooleLatt X)) st
( z in FF & z <= x & z <= y ) )
assume A3: ( x in FF & y in FF ) ; :: thesis: ex z being Element of (LattPOSet (BooleLatt X)) st
( z in FF & z <= x & z <= y )
reconsider x1 = x, y1 = y as Element of (BooleLatt X) ;
set z = x1 "/\" y1;

A4: now :: thesis: ( (x1 "/\" y1) % <= x1 % & (x1 "/\" y1) % <= y1 % )

( 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: verum

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: verum

end;

hence FF is filtered ; :: thesis: verum

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: ( x in FF & x <= y implies y in FF )
assume A5: ( x in FF & x <= y ) ; :: thesis: y in FF
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: verum

end;

hence FF is upper ; :: thesis: verum

end;

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

end;

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