let R be non empty right_unital left_unital doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of R holds
( I is proper iff for u being Element of R st u is unital holds
not u in I )
let I be non empty right-ideal Subset of R; :: thesis: ( I is proper iff for u being Element of R st u is unital holds
not u in I )

A1: now :: thesis: ( I is proper implies for u being Element of R st u is unital holds
not u in I )

assume A2: I is proper ; :: thesis: for u being Element of R st u is unital holds
not u in I
A3: not 1. R in I

proof

assume A4: 1. R in I ; :: thesis: contradiction

A5: now :: thesis: for u being object st u in the carrier of R holds
u in I

let u be object ; :: thesis: ( u in the carrier of R implies u in I )
assume u in the carrier of R ; :: thesis: u in I
then reconsider u9 = u as Element of R ;
(1. R) * u9 = u9 ;
hence u in I by A4, Def3; :: thesis: verum

end;

for u being object st u in I holds
u in the carrier of R ;
then I = the carrier of R by A5, TARSKI:2;
hence contradiction by A2, SUBSET_1:def 6; :: thesis: verum

end;

thus for u being Element of R st u is unital holds
not u in I :: thesis: verum

proof

let u be Element of R; :: thesis: ( u is unital implies not u in I )
assume u is unital ; :: thesis: not u in I
then ex b being Element of R st
( 1. R = u * b & 1. R = b * u ) by GCD_1:def 2;
hence not u in I by A3, Def3; :: thesis: verum

end;

end;

now :: thesis: ( ( for u being Element of R st u is unital holds
not u in I ) implies I is proper )

1. R = (1. R) * (1. R) ;
then A6: 1. R is unital by GCD_1:def 2;
assume for u being Element of R st u is unital holds
not u in I ; :: thesis: I is proper
then I <> the carrier of R by A6;
hence I is proper by SUBSET_1:def 6; :: thesis: verum

end;

hence ( I is proper iff for u being Element of R st u is unital holds
not u in I ) by A1; :: thesis: verum