consider a being Element of C;
reconsider b = Fin a as Subset of C by Lm3;
take b ; :: thesis: ( b is preBoolean & not b is empty )
thus ( b is preBoolean & not b is empty ) ; :: thesis: verum