reconsider T = the topology of X as Subset-Family of X ;
take T ; :: thesis: ( T c= the topology of X & ex F being Basis of X st F c= FinMeetCl T )
thus T c= the topology of X ; :: thesis: ex F being Basis of X st F c= FinMeetCl T
reconsider F = the topology of X as Basis of X by Th2;
take F ; :: thesis: F c= FinMeetCl T
thus F c= FinMeetCl T by Th4; :: thesis: verum