let X, Y be set ; :: thesis: ( X c= Y implies ( proj1 X c= proj1 Y & proj2 X c= proj2 Y ) )
assume A1: for x being set st x in X holds
x in Y ; :: according to TARSKI:def 3 :: thesis: ( proj1 X c= proj1 Y & proj2 X c= proj2 Y )
thus proj1 X c= proj1 Y :: thesis: proj2 X c= proj2 Y

proof

let x be set ; :: 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 set such that
A2: [x,y] in X by RELAT_1:def 4;
[x,y] in Y by A1, A2;
hence x in proj1 Y by RELAT_1:def 4; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 X or y in proj2 Y )
assume y in proj2 X ; :: thesis: y in proj2 Y
then consider x being set such that
A3: [x,y] in X by RELAT_1:def 5;
[x,y] in Y by A1, A3;
hence y in proj2 Y by RELAT_1:def 5; :: thesis: verum