set C = the 1 -element Subset of L;
reconsider C = the 1 -element Subset of L as strict_chain of R by Th1;
take C ; :: thesis: C is 1 -element
thus C is 1 -element ; :: thesis: verum