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