let L, S be RelStr ; :: thesis: ( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )
A1: ( (the InternalRel of L |_2 the carrier of S) ~ = (the InternalRel of L ~ ) |_2 the carrier of S & ((the InternalRel of L ~ ) |_2 the carrier of S) ~ = ((the InternalRel of L ~ ) ~ ) |_2 the carrier of S ) by ORDERS_1:193;

hereby :: thesis: ( ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )

assume S is full SubRelStr of L ; :: thesis: S opp is full SubRelStr of L opp
then ( S opp is SubRelStr of L opp & the InternalRel of S = the InternalRel of L |_2 the carrier of S ) by Th3, YELLOW_0:def 14;
hence S opp is full SubRelStr of L opp by A1, YELLOW_0:def 14; :: thesis: verum

end;

hereby :: thesis: ( S opp is full SubRelStr of L iff S is full SubRelStr of L opp )

assume S opp is full SubRelStr of L opp ; :: thesis: S is full SubRelStr of L
then ( S is SubRelStr of L & the InternalRel of (S opp ) = the InternalRel of (L opp ) |_2 the carrier of S ) by Th3, YELLOW_0:def 14;
hence S is full SubRelStr of L by A1, YELLOW_0:def 14; :: thesis: verum

end;

hereby :: thesis: ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L )

assume S opp is full SubRelStr of L ; :: thesis: S is full SubRelStr of L opp
then ( S is SubRelStr of L opp & the InternalRel of (S opp ) = the InternalRel of L |_2 the carrier of S ) by Th3, YELLOW_0:def 14;
hence S is full SubRelStr of L opp by A1, YELLOW_0:def 14; :: thesis: verum

end;

assume S is full SubRelStr of L opp ; :: thesis: S opp is full SubRelStr of L
then ( S opp is SubRelStr of L & the InternalRel of S = the InternalRel of (L opp ) |_2 the carrier of S ) by Th3, YELLOW_0:def 14;
hence S opp is full SubRelStr of L by A1, YELLOW_0:def 14; :: thesis: verum