let X1, X2, X3, X4 be non empty set ; :: thesis: for x being Element of [:X1,X2,X3,X4:] holds
( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )
let x be Element of [:X1,X2,X3,X4:]; :: thesis: ( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )
reconsider Y = [:X1,X2:], X3 = X3, X4 = X4 as non empty set ;
reconsider x9 = x as Element of [:Y,X3,X4:] by Th38;
set Z9 = {(x `1_4),(x `2_4)};
set Z = {{(x `1_4),(x `2_4)},{(x `1_4)}};
set Y9 = {{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)};
set Y = {{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}};
set X9 = {{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)};
set X = {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}};
x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)]
.= {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}} ;
then ( ( x = x `1_4 or x = x `2_4 ) implies ( {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}} in {(x `1_4),(x `2_4)} & {(x `1_4),(x `2_4)} in {{(x `1_4),(x `2_4)},{(x `1_4)}} & {{(x `1_4),(x `2_4)},{(x `1_4)}} in {{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)} & {{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)} in {{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}} & {{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}} in {{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)} & {{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)} in {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}} ) ) by TARSKI:def 2;
hence ( x <> x `1_4 & x <> x `2_4 ) by XREGULAR:10; :: thesis: ( x <> x `3_4 & x <> x `4_4 )
x `3_4 = (x `1) `2
.= x9 `2_3 ;
hence ( x <> x `3_4 & x <> x `4_4 ) by Th35; :: thesis: verum