let k be Element of NAT ; :: thesis: PFBrt 1,k = {(PFArt 1,k),(PFCrt 1,k)}
thus PFBrt 1,k c= {(PFArt 1,k),(PFCrt 1,k)} :: according to XBOOLE_0:def 10 :: thesis: {(PFArt 1,k),(PFCrt 1,k)} c= PFBrt 1,k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFBrt 1,k or x in {(PFArt 1,k),(PFCrt 1,k)} )
assume A1: x in PFBrt 1,k ; :: thesis: x in {(PFArt 1,k),(PFCrt 1,k)}

per cases ( ex m being non empty Element of NAT st
( m <= 1 & x = PFArt m,k ) or x = PFCrt 1,k ) by A1, Def4;

suppose ex m being non empty Element of NAT st
( m <= 1 & x = PFArt m,k ) ; :: thesis: x in {(PFArt 1,k),(PFCrt 1,k)}

then consider m being non empty Element of NAT such that
A2: ( m <= 1 & x = PFArt m,k ) ;
m >= 1 by NAT_1:14;
then m = 1 by A2, XXREAL_0:1;
hence x in {(PFArt 1,k),(PFCrt 1,k)} by A2, TARSKI:def 2; :: thesis: verum

end;

suppose x = PFCrt 1,k ; :: thesis: x in {(PFArt 1,k),(PFCrt 1,k)}

hence x in {(PFArt 1,k),(PFCrt 1,k)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(PFArt 1,k),(PFCrt 1,k)} or x in PFBrt 1,k )
assume A3: x in {(PFArt 1,k),(PFCrt 1,k)} ; :: thesis: x in PFBrt 1,k

per cases ( x = PFArt 1,k or x = PFCrt 1,k ) by A3, TARSKI:def 2;

suppose x = PFArt 1,k ; :: thesis: x in PFBrt 1,k

hence x in PFBrt 1,k by Def4; :: thesis: verum

end;

suppose x = PFCrt 1,k ; :: thesis: x in PFBrt 1,k

hence x in PFBrt 1,k by Def4; :: thesis: verum

end;

end;