let X be infinite set ; :: thesis: for U, V being non empty open Subset of (ClFinTop X) holds U meets V
let U, V be non empty open Subset of (ClFinTop X); :: thesis: U meets V
assume U misses V ; :: thesis: contradiction
then ( U c= V ` & V ` is finite ) by Th34, SUBSET_1:43;
then A1: ( U is finite & the carrier of (ClFinTop X) = X ) by Def6;
then not U ` is finite by Th35;
then U ` = [#] the carrier of (ClFinTop X) by A1, Def6;
then (U ` ) ` = {} the carrier of (ClFinTop X) by XBOOLE_1:37;
hence contradiction ; :: thesis: verum