let Y be non empty set ; :: thesis: ( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y )
A1: for x being Element of Y holds ('not' (O_el Y)) . x = TRUE

proof

let x be Element of Y; :: thesis: ('not' (O_el Y)) . x = TRUE
( ('not' (O_el Y)) . x = 'not' ((O_el Y) . x) & (O_el Y) . x = FALSE ) by Def10, MARGREL1:def 19;
hence ('not' (O_el Y)) . x = TRUE ; :: thesis: verum

end;

for x being Element of Y holds ('not' (I_el Y)) . x = FALSE

proof

let x be Element of Y; :: thesis: ('not' (I_el Y)) . x = FALSE
( ('not' (I_el Y)) . x = 'not' ((I_el Y) . x) & (I_el Y) . x = TRUE ) by Def11, MARGREL1:def 19;
hence ('not' (I_el Y)) . x = FALSE ; :: thesis: verum

end;

hence ( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y ) by A1, Def10, Def11; :: thesis: verum