let T be non empty TopSpace; :: thesis: the topology of T = FinMeetCl the topology of T
set X = the topology of T;
defpred S1[ set ] means meet $1 in the topology of T;
A1: for B9 being Element of Fin the topology of T
for b being Element of the topology of T st S1[B9] holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin the topology of T; :: thesis: for b being Element of the topology of T st S1[B9] holds
S1[B9 \/ {b}]
let b be Element of the topology of T; :: thesis: ( S1[B9] implies S1[B9 \/ {b}] )
A2: meet {b} = b by SETFAM_1:10;
assume A3: meet B9 in the topology of T ; :: thesis: S1[B9 \/ {b}]
per cases ( B9 <> {} or B9 = {} ) ;
end;
end;
thus the topology of T c= FinMeetCl the topology of T by Th4; :: according to XBOOLE_0:def 10 :: thesis: FinMeetCl the topology of T c= the topology of T
A4: S1[ {}. the topology of T] by PRE_TOPC:1, SETFAM_1:1;
A5: for B being Element of Fin the topology of T holds S1[B] from SETWISEO:sch 4(A4, A1);
now :: thesis: for x being Subset of T st x in FinMeetCl the topology of T holds
x in the topology of T
let x be Subset of T; :: thesis: ( x in FinMeetCl the topology of T implies b1 in the topology of T )
assume x in FinMeetCl the topology of T ; :: thesis: b1 in the topology of T
then consider y being Subset-Family of T such that
A6: ( y c= the topology of T & y is finite ) and
A7: x = Intersect y by Def3;
reconsider y = y as Subset-Family of T ;
per cases ( y <> {} or y = {} ) ;
suppose A10: y = {} ; :: thesis: b1 in the topology of T
reconsider aa = {} (bool the carrier of T) as Subset-Family of the carrier of T ;
Intersect aa = the carrier of T by SETFAM_1:def 9;
hence x in the topology of T by A7, A10, PRE_TOPC:def 1; :: thesis: verum
end;
end;
end;
hence FinMeetCl the topology of T c= the topology of T ; :: thesis: verum