let X1, X2, X3 be non empty set ; :: thesis: for x being Element of [:X1,X2,X3:] holds
( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )
let x be Element of [:X1,X2,X3:]; :: thesis: ( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )
set Y9 = {(x `1_3),(x `2_3)};
set Y = {{(x `1_3),(x `2_3)},{(x `1_3)}};
set X9 = {{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)};
set X = {{{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)},{{{(x `1_3),(x `2_3)},{(x `1_3)}}}};
A1: x = [(x `1_3),(x `2_3),(x `3_3)]
.= [[(x `1_3),(x `2_3)],(x `3_3)] ;
then ( ( x = x `1_3 or x = x `2_3 ) implies ( {{{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)},{{{(x `1_3),(x `2_3)},{(x `1_3)}}}} in {(x `1_3),(x `2_3)} & {(x `1_3),(x `2_3)} in {{(x `1_3),(x `2_3)},{(x `1_3)}} & {{(x `1_3),(x `2_3)},{(x `1_3)}} in {{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)} & {{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)} in {{{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)},{{{(x `1_3),(x `2_3)},{(x `1_3)}}}} ) ) by TARSKI:def 2;
hence ( x <> x `1_3 & x <> x `2_3 ) by XREGULAR:8; :: thesis: x <> x `3_3
thus x <> x `3_3 by A1, Th14; :: thesis: verum