let X be set ; :: thesis: 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):] )
let A be Subset of X; :: thesis: ( X = {1,2,3} & A = {1} implies ( [2,1] in [:(X \ A),X:] \/ [:X,A:] & not [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):] ) )
assume that
A1: X = {1,2,3} and
A2: A = {1} ; :: thesis: ( [2,1] in [:(X \ A),X:] \/ [:X,A:] & not [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):] )
( 1 in X & 2 in X \ A ) by A1, A2, Th32, TARSKI:def 2, ENUMSET1:def 1;
then [2,1] in [:(X \ A),X:] by ZFMISC_1:87;
hence [2,1] in [:(X \ A),X:] \/ [:X,A:] by XBOOLE_0:def 3; :: thesis: not [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):]
assume [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):] ; :: thesis: contradiction
then ( [2,1] in [:A,A:] or [2,1] in [:(X \ A),(X \ A):] ) by XBOOLE_0:def 3;
then ( 2 in {1} or 1 in {2,3} ) by A1, A2, Th32, ZFMISC_1:87;
hence contradiction by TARSKI:def 1, TARSKI:def 2; :: thesis: verum