let R be non empty right_unital doubleLoopStr ; :: thesis: for I being non empty left-ideal Subset of R holds
( I is proper iff not 1. R in I )
let I be non empty left-ideal Subset of R; :: thesis: ( I is proper iff not 1. R in I )

A1: now :: thesis: ( I is proper implies not 1. R in I )

assume A2: I is proper ; :: thesis: not 1. R in I
thus not 1. R in I :: thesis: verum

proof

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

A4: 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 ;
u9 * (1. R) = u9 ;
hence u in I by A3, Def2; :: 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 A4, TARSKI:2;
hence contradiction by A2, SUBSET_1:def 6; :: thesis: verum

end;

end;

now :: thesis: ( not 1. R in I implies I is proper )

assume not 1. R in I ; :: thesis: I is proper
then I <> the carrier of R ;
hence I is proper by SUBSET_1:def 6; :: thesis: verum

end;

hence ( I is proper iff not 1. R in I ) by A1; :: thesis: verum