let n be Element of NAT ; PFArt (1,n) = {[1,n],[2,n]}
thus
PFArt (1,n) c= {[1,n],[2,n]}
XBOOLE_0:def 10 {[1,n],[2,n]} c= PFArt (1,n)
let x be object ; TARSKI:def 3 ( not x in {[1,n],[2,n]} or x in PFArt (1,n) )
assume A3:
x in {[1,n],[2,n]}
; x in PFArt (1,n)