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)) = [:{(1 / 2)},[.0 ,1.]:] )
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)) = [:{(1 / 2)},[.0 ,1.]:]
([#] ([: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:122
.= [:{(1 / 2)},[.0 ,1.]:] by XXREAL_1:418 ;
hence ([#] ([:I[01] ,I[01] :] | A)) /\ ([#] ([:I[01] ,I[01] :] | B)) = [:{(1 / 2)},[.0 ,1.]:] ; :: thesis: verum