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