{} c= the carrier of E ;
then reconsider T = {} as Subset of the carrier of E ;
take T ; :: thesis: ( T is finite & T is F -algebraic )
thus ( T is finite & T is F -algebraic ) ; :: thesis: verum