let T be non empty TopSpace; :: thesis: the topology of T = FinMeetCl the topology of T
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
set X = the topology of T;
defpred S₁[ set ] means meet $1 in the topology of T;
A1: S₁[ {}. the topology of T] by PRE_TOPC:5, SETFAM_1:2;
A2: for B' being Element of Fin the topology of T
for b being Element of the topology of T st S₁[B'] holds
S₁[B' \/ {b}]

proof

let B' be Element of Fin the topology of T; :: thesis: for b being Element of the topology of T st S₁[B'] holds
S₁[B' \/ {b}]
let b be Element of the topology of T; :: thesis: ( S₁[B'] implies S₁[B' \/ {b}] )
A3: meet {b} = b by SETFAM_1:11;
assume A4: meet B' in the topology of T ; :: thesis: S₁[B' \/ {b}]

per cases ( B' <> {} or B' = {} ) ;

suppose B' <> {} ; :: thesis: S₁[B' \/ {b}]

then meet (B' \/ {b}) = (meet B') /\ (meet {b}) by SETFAM_1:10;
hence meet (B' \/ {b}) in the topology of T by A3, A4, PRE_TOPC:def 1; :: thesis: verum

end;

suppose B' = {} ; :: thesis: S₁[B' \/ {b}]

hence meet (B' \/ {b}) in the topology of T by A3; :: thesis: verum

end;

end;

end;

A5: for B being Element of Fin the topology of T holds S₁[B] from SETWISEO:sch 4(A1, A2);

now

let x be Subset of T; :: thesis: ( x in FinMeetCl the topology of T implies b₁ in the topology of T )
assume x in FinMeetCl the topology of T ; :: thesis: b₁ 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 & x = Intersect y ) by Def4;
reconsider y = y as Subset-Family of T ;

per cases ( y <> {} or y = {} ) ;

suppose y <> {} ; :: thesis: b₁ in the topology of T

then A7: x = meet y by A6, SETFAM_1:def 10;
y in Fin the topology of T by A6, FINSUB_1:def 5;
hence x in the topology of T by A5, A7; :: thesis: verum

end;

suppose A8: y = {} ; :: thesis: b₁ 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 10;
hence x in the topology of T by A6, A8, PRE_TOPC:def 1; :: thesis: verum

end;

end;

end;

hence FinMeetCl the topology of T c= the topology of T by SUBSET_1:7; :: thesis: verum