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