let X be non empty set ; :: thesis: for F1, F2, F being Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2 holds
for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty
let F1, F2 be Filter of X; :: thesis: for F being Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2 holds
for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty
let F be Filter of X; :: thesis: ( F is_filter-finer_than F1 & F is_filter-finer_than F2 implies for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty )
assume that
A1: F is_filter-finer_than F1 and
A2: F is_filter-finer_than F2 ; :: thesis: for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty

hereby :: thesis: verum

let M1 be Element of F1; :: thesis: for M2 being Element of F2 holds not M1 /\ M2 is empty
let M2 be Element of F2; :: thesis: not M1 /\ M2 is empty
( M1 in F1 & M2 in F2 ) ;
then M1 /\ M2 in F by A1, A2, CARD_FIL:def 1;
hence not M1 /\ M2 is empty by CARD_FIL:def 1; :: thesis: verum

end;