let n be Element of NAT ; :: thesis: PFArt 1,n = {[1,n],[2,n]}
thus PFArt 1,n c= {[1,n],[2,n]} :: according to XBOOLE_0:def 10 :: thesis: {[1,n],[2,n]} c= PFArt 1,n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFArt 1,n or x in {[1,n],[2,n]} )
assume A1: x in PFArt 1,n ; :: thesis: x in {[1,n],[2,n]}

per cases ( ex m being odd Element of NAT st
( m <= 2 * 1 & [m,n] = x ) or [(2 * 1),n] = x ) by A1, Def2;

suppose ex m being odd Element of NAT st
( m <= 2 * 1 & [m,n] = x ) ; :: thesis: x in {[1,n],[2,n]}

then consider m being odd Element of NAT such that
A2: ( m <= 2 * 1 & [m,n] = x ) ;
x = [1,n] by A2, Lm2, NAT_1:27;
hence x in {[1,n],[2,n]} by TARSKI:def 2; :: thesis: verum

end;

suppose [(2 * 1),n] = x ; :: thesis: x in {[1,n],[2,n]}

hence x in {[1,n],[2,n]} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[1,n],[2,n]} or x in PFArt 1,n )
assume A3: x in {[1,n],[2,n]} ; :: thesis: x in PFArt 1,n

per cases ( x = [1,n] or x = [2,n] ) by A3, TARSKI:def 2;

suppose A4: x = [1,n] ; :: thesis: x in PFArt 1,n

1 <= 2 * 1 ;
hence x in PFArt 1,n by A4, Def2, Lm3; :: thesis: verum

end;

suppose x = [2,n] ; :: thesis: x in PFArt 1,n

then x = [(2 * 1),n] ;
hence x in PFArt 1,n by Def2; :: thesis: verum

end;

end;