set C = the non empty trivial Subset of L;
reconsider C = the non empty trivial Subset of L as strict_chain of R by Th4;
take C ; :: thesis: ( not C is empty & C is trivial )
thus ( not C is empty & C is trivial ) ; :: thesis: verum