let T be non empty TopSpace; :: thesis: the topology of T = FinMeetCl the topology of T
set X = the topology of T;
defpred S₁[ 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 S₁[B9] holds
S₁[B9 \/ {b}]

proof

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

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

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

then meet (B9 \/ {b}) = (meet B9) /\ (meet {b}) by SETFAM_1:9;
hence S₁[B9 \/ {b}] by A2, A3, PRE_TOPC:def 1; :: thesis: verum

end;

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

hence S₁[B9 \/ {b}] by A2; :: thesis: verum

end;

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: S₁[ {}. the topology of T] by PRE_TOPC:1, SETFAM_1:1;
A5: for B being Element of Fin the topology of T holds S₁[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 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 ) and
A7: x = Intersect y by Def3;
reconsider y = y as Subset-Family of T ;

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

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

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

end;

suppose A10: 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 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