let X, Y be non empty Subset of ExtREAL ; :: thesis: ( X c= Y iff - X c= - Y )

hereby :: thesis: ( - X c= - Y implies X c= Y )

assume A1: X c= Y ; :: thesis: - X c= - Y
thus - X c= - Y :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in - X or x in - Y )
assume A2: x in - X ; :: thesis: x in - Y
then reconsider x = x as R_eal ;
- x in - (- X) by A2, Th23;
then - x in X by Th22;
then - (- x) in - Y by A1, Th23;
hence x in - Y ; :: thesis: verum

end;

end;

assume A3: - X c= - Y ; :: thesis: X c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A4: x in X ; :: thesis: x in Y
then reconsider x = x as R_eal ;
- x in - X by A4, Th23;
hence x in Y by A3, Th23; :: thesis: verum