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 that
A1: A = [:[.0 ,(1 / 2).],[.0 ,1.]:] and
A2: 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 10
.= A \/ B by PRE_TOPC:def 10
.= [:([.0 ,(1 / 2).] \/ [.(1 / 2),1.]),[.0 ,1.]:] by A1, A2, ZFMISC_1:120
.= [:[.0 ,1.],[.0 ,1.]:] by XXREAL_1:174
.= [#] [:I[01] ,I[01] :] by BORSUK_1:83, BORSUK_1:def 5 ;
hence ([#] ([:I[01] ,I[01] :] | A)) \/ ([#] ([:I[01] ,I[01] :] | B)) = [#] [:I[01] ,I[01] :] ; :: thesis: verum