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 U ` is infinite 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

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 U ` is infinite 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