let L, S be RelStr ; :: thesis: ( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )
thus ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) :: thesis: ( ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) ) thus ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) :: thesis: ( S opp is SubRelStr of L iff S is SubRelStr of L opp ) thus ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) :: thesis: ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) assume that
A7: the carrier of S c= the carrier of (L opp) and
A8: the InternalRel of S c= the InternalRel of (L opp) ; :: according to YELLOW_0:def 13 :: thesis: S opp is SubRelStr of L
thus ( the carrier of (S opp) c= the carrier of L & the InternalRel of (S opp) c= the InternalRel of L ) by A7, A8, Th1; :: according to YELLOW_0:def 13 :: thesis: verum