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 object ; :: 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 ) ;
not not m = 0 & ... & not m = 2 by A2;
then x = [1,n] by A2;
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 object ; :: 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, Lm2, 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;