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 that
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) and
A2: 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 ) )
A3: the carrier of R c= the carrier of T2 by A1, A2, YELLOW_0:def 13;
A4: the InternalRel of R c= the InternalRel of T2 by A1, A2, YELLOW_0:def 13;
hence R is SubRelStr of T2 by A3, YELLOW_0:def 13; :: thesis: ( S is full implies R is full SubRelStr of T2 )
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, A3, A4, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum