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

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