consider C being non empty trivial Subset of L;
reconsider C = C 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