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 that
A1: x <= y and
A2: y <= x ; :: thesis: x = y
A3: the carrier of S c= the carrier of L by Def13;
[x,y] in the InternalRel of S by A1;
then ( x in the carrier of S & y in the carrier of S ) by ZFMISC_1:87;
then reconsider a = x, b = y as Element of L by A3;
( a <= b & b <= a ) by A1, A2, Th59;
hence x = y by ORDERS_2:2; :: thesis: verum