let A, B be Subset of [:I[01],I[01]:]; :: thesis: ( A = [:[.0,(1 / 2).],[.0,1.]:] & B = [:[.(1 / 2),1.],[.0,1.]:] implies ([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = [#] [:I[01],I[01]:] )
assume A1: ( A = [:[.0,(1 / 2).],[.0,1.]:] & B = [:[.(1 / 2),1.],[.0,1.]:] ) ; :: thesis: ([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = [#] [:I[01],I[01]:]
([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = A \/ ([#] ([:I[01],I[01]:] | B)) by PRE_TOPC:def 5
.= A \/ B by PRE_TOPC:def 5
.= [:([.0,(1 / 2).] \/ [.(1 / 2),1.]),[.0,1.]:] by A1, ZFMISC_1:97
.= [:[.0,1.],[.0,1.]:] by XXREAL_1:174
.= [#] [:I[01],I[01]:] by BORSUK_1:40, BORSUK_1:def 2 ;
hence ([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = [#] [:I[01],I[01]:] ; :: thesis: verum