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 object ; :: 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 zero Element of NAT st
( m <= 1 & x = PFArt (m,k) ) or x = PFCrt (1,k) ) by A1, Def4;

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

then consider m being non zero Element of NAT such that
A2: m <= 1 and
A3: 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 A3, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(PFArt (1,k)),(PFCrt (1,k))} or x in PFBrt (1,k) )
assume A4: 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 A4, 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;