let S be full SubRelStr of L; :: thesis: S is reflexive
let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of S or [x,x] in the InternalRel of S )
assume A1: x in the carrier of S ; :: thesis: [x,x] in the InternalRel of S
then A2: [x,x] in [: the carrier of S, the carrier of S:] by ZFMISC_1:87;
( the carrier of S c= the carrier of L & the InternalRel of L is_reflexive_in the carrier of L ) by Def13, ORDERS_2:def 2;
then A3: [x,x] in the InternalRel of L by A1;
the InternalRel of S = the InternalRel of L |_2 the carrier of S by Def14;
hence [x,x] in the InternalRel of S by A2, A3, XBOOLE_0:def 4; :: thesis: verum