let A, B be Subset of [:I[01] ,I[01] :]; ( 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.]:] )
; ([#] ([: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, 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] :]
; verum