let X, Y be set ; :: thesis: ( X c= Y implies proj2 X c= proj2 Y )
assume A1: X c= Y ; :: thesis: proj2 X c= proj2 Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj2 X or x in proj2 Y )
assume x in proj2 X ; :: thesis: x in proj2 Y
then consider y being object such that
A2: [y,x] in X by Def13;
[y,x] in Y by A1, A2;
hence x in proj2 Y by Def13; :: thesis: verum