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 by ORDERS_1:83;

then the InternalRel of S = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def 14;

hence S opp is full SubRelStr of L by A1, A6, Th2, YELLOW_0:def 14; :: thesis: verum

A1: ( the InternalRel of L |_2 the carrier of S) ~ = ( the InternalRel of L ~) |_2 the carrier of S by ORDERS_1:83;

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

A3:
(( the InternalRel of L ~) |_2 the carrier of S) ~ = (( the InternalRel of L ~) ~) |_2 the carrier of S
by ORDERS_1:83;assume A2:
S is full SubRelStr of L
; :: thesis: S opp is full SubRelStr of L opp

then the InternalRel of S = the InternalRel of L |_2 the carrier of S by YELLOW_0:def 14;

hence S opp is full SubRelStr of L opp by A1, A2, Th2, YELLOW_0:def 14; :: thesis: verum

end;then the InternalRel of S = the InternalRel of L |_2 the carrier of S by YELLOW_0:def 14;

hence S opp is full SubRelStr of L opp by A1, A2, Th2, YELLOW_0:def 14; :: thesis: verum

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

assume A4:
S opp is full SubRelStr of L opp
; :: thesis: S is full SubRelStr of L

then the InternalRel of (S opp) = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def 14;

hence S is full SubRelStr of L by A3, A4, Th2, YELLOW_0:def 14; :: thesis: verum

end;then the InternalRel of (S opp) = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def 14;

hence S is full SubRelStr of L by A3, A4, Th2, YELLOW_0:def 14; :: thesis: verum

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

assume A6:
S is full SubRelStr of L opp
; :: thesis: S opp is full SubRelStr of Lassume A5:
S opp is full SubRelStr of L
; :: thesis: S is full SubRelStr of L opp

then the InternalRel of (S opp) = the InternalRel of L |_2 the carrier of S by YELLOW_0:def 14;

hence S is full SubRelStr of L opp by A1, A5, Th2, YELLOW_0:def 14; :: thesis: verum

end;then the InternalRel of (S opp) = the InternalRel of L |_2 the carrier of S by YELLOW_0:def 14;

hence S is full SubRelStr of L opp by A1, A5, Th2, YELLOW_0:def 14; :: thesis: verum

then the InternalRel of S = the InternalRel of (L opp) |_2 the carrier of S by YELLOW_0:def 14;

hence S opp is full SubRelStr of L by A1, A6, Th2, YELLOW_0:def 14; :: thesis: verum