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