let X be non empty set ; :: thesis: for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) )
let F be non empty Subset of (BooleLatt X); :: thesis: ( F is Filter of (BooleLatt X) iff for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) )

hereby :: thesis: ( ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) implies F is Filter of (BooleLatt X) )

assume A1: F is Filter of (BooleLatt X) ; :: thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) )

hereby :: thesis: verum

let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) )
( Y1 is Element of the carrier of (BooleLatt X) & Y2 is Element of the carrier of (BooleLatt X) ) by LATTICE3:def 1;
hence ( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) by A1, Th31; :: thesis: verum

end;

end;

assume A2: for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ; :: thesis: F is Filter of (BooleLatt X)

now :: thesis: ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) )

hereby :: thesis: for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F

let p, q be Element of F; :: thesis: p /\ q in F
reconsider p1 = p, q1 = q as Subset of X by LATTICE3:def 1;
( p1 in F & q1 in F implies p1 /\ q1 in F ) by A2;
hence p /\ q in F ; :: thesis: verum

end;

let p be Element of F; :: thesis: for q being Element of (BooleLatt X) st p c= q holds
q in F
let q be Element of (BooleLatt X); :: thesis: ( p c= q implies q in F )
assume A3: p c= q ; :: thesis: q in F
reconsider p1 = p, q1 = q as Subset of X by LATTICE3:def 1;
( p1 in F & p1 c= q & ( p1 in F & p1 c= q1 implies q1 in F ) ) by A2, A3;
hence q in F ; :: thesis: verum

end;

hence F is Filter of (BooleLatt X) by Th31; :: thesis: verum