set a = the Element of C;
reconsider b = Fin the Element of C 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