let X be set ; :: thesis: ( Fin X is c=directed & Fin X is c=filtered )

now

let a, b be set ; :: thesis: ( a in Fin X & b in Fin X implies ex c being set st
( a \/ b c= c & c in Fin X ) )
assume ( a in Fin X & b in Fin X ) ; :: thesis: ex c being set st
( a \/ b c= c & c in Fin X )
then ( a c= X & a is finite & b c= X & b is finite ) by FINSUB_1:def 5;
then A1: ( a \/ b c= X & a \/ b is finite ) by XBOOLE_1:8;
take c = a \/ b; :: thesis: ( a \/ b c= c & c in Fin X )
thus a \/ b c= c ; :: thesis: c in Fin X
thus c in Fin X by A1, FINSUB_1:def 5; :: thesis: verum

end;

hence Fin X is c=directed by Th6; :: thesis: Fin X is c=filtered

now

let a, b be set ; :: thesis: ( a in Fin X & b in Fin X implies ex c being set st
( c c= a /\ b & c in Fin X ) )
assume ( a in Fin X & b in Fin X ) ; :: thesis: ex c being set st
( c c= a /\ b & c in Fin X )
reconsider c = {} as set ;
take c = c; :: thesis: ( c c= a /\ b & c in Fin X )
thus c c= a /\ b by XBOOLE_1:2; :: thesis: c in Fin X
thus c in Fin X by FINSUB_1:18; :: thesis: verum

end;

hence Fin X is c=filtered by Th8; :: thesis: verum