thus ( X c= Y implies for e being ext-real number st e in X holds
e in Y ) ; :: thesis: ( ( for e being ext-real number st e in X holds
e in Y ) implies X c= Y )
assume A1: for e being ext-real number st e in X holds
e in Y ; :: thesis: X c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume x in X ; :: thesis: x in Y
hence x in Y by A1; :: thesis: verum