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;