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' (I_el Y)) . x = FALSE

proof

let x be Element of Y; :: thesis: ('not' (I_el Y)) . x = FALSE
A2: ('not' (I_el Y)) . x = 'not' ((I_el Y) . x) by MARGREL1:def 20;
(I_el Y) . x = TRUE by Def14;
hence ('not' (I_el Y)) . x = FALSE by A2; :: thesis: verum

end;

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
A3: ('not' (O_el Y)) . x = 'not' ((O_el Y) . x) by MARGREL1:def 20;
(O_el Y) . x = FALSE by Def13;
hence ('not' (O_el Y)) . x = TRUE by A3; :: thesis: verum

end;

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