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 ) )

proof

assume that
A1: the carrier of S c= the carrier of L and
A2: the InternalRel of S c= the InternalRel of L ; :: according to YELLOW_0:def 13 :: thesis: S opp is SubRelStr of L opp
thus ( the carrier of (S opp) c= the carrier of (L opp) & the InternalRel of (S opp) c= the InternalRel of (L opp) ) by A1, A2, Th1; :: according to YELLOW_0:def 13 :: thesis: verum

end;

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 )

proof

assume that
A3: the carrier of (S opp) c= the carrier of (L opp) and
A4: the InternalRel of (S opp) c= the InternalRel of (L opp) ; :: according to YELLOW_0:def 13 :: thesis: S is SubRelStr of L
thus ( the carrier of S c= the carrier of L & the InternalRel of S c= the InternalRel of L ) by A3, A4, Th1; :: according to YELLOW_0:def 13 :: thesis: verum

end;

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 )

proof

assume that
A5: the carrier of (S opp) c= the carrier of L and
A6: the InternalRel of (S opp) c= the InternalRel of L ; :: according to YELLOW_0:def 13 :: thesis: S is SubRelStr of L opp
thus ( the carrier of S c= the carrier of (L opp) & the InternalRel of S c= the InternalRel of (L opp) ) by A5, A6, Th1; :: according to YELLOW_0:def 13 :: thesis: verum

end;

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