reconsider w = g as left-right by Th4;
take the RightOptions of w ; :: thesis: ex w being left-right st
( g = w & the RightOptions of w = the RightOptions of w )
thus ex w being left-right st
( g = w & the RightOptions of w = the RightOptions of w ) ; :: thesis: verum