let L be reflexive RelStr ; :: thesis: for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds

S1 is SubRelStr of S2

let S1, S2 be full SubRelStr of L; :: thesis: ( the carrier of S1 c= the carrier of S2 implies S1 is SubRelStr of S2 )

assume A1: the carrier of S1 c= the carrier of S2 ; :: thesis: S1 is SubRelStr of S2

hence the carrier of S1 c= the carrier of S2 ; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of S1 c= the InternalRel of S2

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of S1 or [x,y] in the InternalRel of S2 )

assume A2: [x,y] in the InternalRel of S1 ; :: thesis: [x,y] in the InternalRel of S2

then A3: x in the carrier of S1 by ZFMISC_1:87;

reconsider x = x, y = y as Element of S1 by A2, ZFMISC_1:87;

the carrier of S1 c= the carrier of L by YELLOW_0:def 13;

then reconsider a = x, b = y as Element of L by A3;

reconsider x9 = x, y9 = y as Element of S2 by A1, A3;

x <= y by A2;

then a <= b by YELLOW_0:59;

then x9 <= y9 by A1, A3, YELLOW_0:60;

hence [x,y] in the InternalRel of S2 ; :: thesis: verum

S1 is SubRelStr of S2

let S1, S2 be full SubRelStr of L; :: thesis: ( the carrier of S1 c= the carrier of S2 implies S1 is SubRelStr of S2 )

assume A1: the carrier of S1 c= the carrier of S2 ; :: thesis: S1 is SubRelStr of S2

hence the carrier of S1 c= the carrier of S2 ; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of S1 c= the InternalRel of S2

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of S1 or [x,y] in the InternalRel of S2 )

assume A2: [x,y] in the InternalRel of S1 ; :: thesis: [x,y] in the InternalRel of S2

then A3: x in the carrier of S1 by ZFMISC_1:87;

reconsider x = x, y = y as Element of S1 by A2, ZFMISC_1:87;

the carrier of S1 c= the carrier of L by YELLOW_0:def 13;

then reconsider a = x, b = y as Element of L by A3;

reconsider x9 = x, y9 = y as Element of S2 by A1, A3;

x <= y by A2;

then a <= b by YELLOW_0:59;

then x9 <= y9 by A1, A3, YELLOW_0:60;

hence [x,y] in the InternalRel of S2 ; :: thesis: verum