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)) = [:{(1 / 2)},[.0 ,1.]:] )
assume A1:
( A = [:[.0 ,(1 / 2).],[.0 ,1.]:] & B = [:[.(1 / 2),1.],[.0 ,1.]:] )
; ([#] ([: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, 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.]:]
; verum