thus ( X c= Y implies for N being ExtNat st N in X holds
N in Y ) ; :: thesis: ( ( for N being ExtNat st N in X holds
N in Y ) implies X c= Y )
assume A1: for N being ExtNat st N in X holds
N in Y ; :: thesis: X c= Y
for x being object st x in X holds
x in Y by A1;
hence X c= Y by TARSKI:def 3; :: thesis: verum