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 set ; :: 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 & y in the carrier of S1 ) by ZFMISC_1:106;
reconsider x = x, y = y as Element of S1 by A2, ZFMISC_1:106;
reconsider x' = x, y' = y as Element of S2 by A1, A3;
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;
x <= y by A2, ORDERS_2:def 9;
then ( x' in the carrier of S2 & y' in the carrier of S2 & a <= b ) by A1, A3, YELLOW_0:60;
then x' <= y' by YELLOW_0:61;
hence [x,y] in the InternalRel of S2 by ORDERS_2:def 9; :: thesis: verum