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