consider a being Element of L;
take {a} ; :: thesis: ( not {a} is empty & {a} is trivial )
thus ( not {a} is empty & {a} is trivial ) ; :: thesis: verum