let T, T2, R be RelStr ; :: thesis: for S being SubRelStr of T st RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) holds
( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )
let S be SubRelStr of T; :: thesis: ( RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) implies ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) ) )
assume A1: ( RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) ) ; :: thesis: ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )
thus A2: R is SubRelStr of T2 :: thesis: ( S is full implies R is full SubRelStr of T2 )

proof

thus ( the carrier of R c= the carrier of T2 & the InternalRel of R c= the InternalRel of T2 ) by A1, YELLOW_0:def 13; :: according to YELLOW_0:def 13 :: thesis: verum

end;

assume the InternalRel of S = the InternalRel of T |_2 the carrier of S ; :: according to YELLOW_0:def 14 :: thesis: R is full SubRelStr of T2
hence R is full SubRelStr of T2 by A1, A2, YELLOW_0:def 14; :: thesis: verum