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