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;
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 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;
A3: (( 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 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;
hereby :: thesis: ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L )
assume 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;
assume A6: S is full SubRelStr of L opp ; :: thesis: S opp is full SubRelStr of L
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