theorem :: UNIFORM3:3

for X being set
for A being Subset of X st X = {1,2,3} & A = {1} holds
( [2,1] in [:(X \ A),X:] \/ [:X,A:] & not [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):] )