reconsider F2 = F as non empty Subset of F by XBOOLE_0:def 10;
take F2 ; :: thesis: F2 is filter_basis
thus F2 is filter_basis ; :: thesis: verum