assume A1: A = F ; :: thesis: -- A = -- F
let a be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not a in -- A or a in -- F ) & ( not a in -- F or a in -- A ) )
hereby :: thesis: ( not a in -- F or a in -- A )
assume A2: a in -- A ; :: thesis: a in -- F
then reconsider b = a as Real ;
- b in A by A2, Th12;
hence a in -- F by A1, Th2; :: thesis: verum
end;
assume a in -- F ; :: thesis: a in -- A
then consider w being Element of ExtREAL such that
A3: a = - w and
A4: w in F ;
reconsider b = w as Real by A1, A4;
- b in -- A by A1, A4;
hence a in -- A by A3; :: thesis: verum