let S be full SubRelStr of L; :: thesis: S is antisymmetric
let x, y be Element of S; :: according to YELLOW_0:def 3 :: thesis: ( x <= y & y <= x implies x = y )
assume A1: ( x <= y & y <= x ) ; :: thesis: x = y
then [x,y] in the InternalRel of S by ORDERS_2:def 9;
then A2: ( x in the carrier of S & y in the carrier of S ) by ZFMISC_1:106;
the carrier of S c= the carrier of L by Def13;
then reconsider a = x, b = y as Element of L by A2;
( a <= b & b <= a ) by A1, Th60;
hence x = y by ORDERS_2:25; :: thesis: verum