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 A1: U c= V ` by SUBSET_1:23;
A2: the carrier of (ClFinTop X) = X by Def6;
V ` is finite by Th34;
then not U ` is finite by A1, A2, Th35;
then U ` = [#] the carrier of (ClFinTop X) by A2, Def6;
then (U `) ` = {} the carrier of (ClFinTop X) by XBOOLE_1:37;
hence contradiction ; :: thesis: verum