now :: thesis: for A being Am of R ex b₂ being non empty Subset of R st
( b₂ is Am of R & 1. R in b₂ )

let A be Am of R; :: thesis: ex b₁ being non empty Subset of R st
( b₁ is Am of R & 1. R in b₁ )
consider x being Element of A such that
A1: x is_associated_to 1. R by Def7;
set A9 = { z where z is Element of A : z <> x } \/ {(1. R)};
1. R in {(1. R)} by TARSKI:def 1;
then A2: 1. R in { z where z is Element of A : z <> x } \/ {(1. R)} by XBOOLE_0:def 3;
reconsider A9 = { z where z is Element of A : z <> x } \/ {(1. R)} as non empty set ;
A3: for x being Element of A9 holds
( x = 1. R or x in A )

proof

let y be Element of A9; :: thesis: ( y = 1. R or y in A )

per cases ( y in { z where z is Element of A : z <> x } or y in {(1. R)} ) by XBOOLE_0:def 3;

suppose y in { z where z is Element of A : z <> x } ; :: thesis: ( y = 1. R or y in A )

then ex zz being Element of A st
( y = zz & zz <> x ) ;
hence ( y = 1. R or y in A ) ; :: thesis: verum

end;

suppose y in {(1. R)} ; :: thesis: ( y = 1. R or y in A )

hence ( y = 1. R or y in A ) by TARSKI:def 1; :: thesis: verum

end;

end;

end;

now :: thesis: for x being object st x in A9 holds
x in the carrier of R

let x be object ; :: thesis: ( x in A9 implies x in the carrier of R )

now :: thesis: ( x in A9 & x in A9 implies x in the carrier of R )

assume A4: x in A9 ; :: thesis: ( x in A9 implies x in the carrier of R )
x in the carrier of R

proof

now :: thesis: ( ( x = 1. R & x in the carrier of R ) or ( x in A & x in the carrier of R ) )

per cases ( x = 1. R or x in A ) by A3, A4;

case x = 1. R ; :: thesis: x in the carrier of R

hence x in the carrier of R ; :: thesis: verum

end;

case x in A ; :: thesis: x in the carrier of R

hence x in the carrier of R ; :: thesis: verum

end;

end;

end;

hence x in the carrier of R ; :: thesis: verum

end;

hence ( x in A9 implies x in the carrier of R ) ; :: thesis: verum

end;

hence ( x in A9 implies x in the carrier of R ) ; :: thesis: verum

end;

then reconsider A9 = A9 as non empty Subset of R by TARSKI:def 3;
A5: for z, y being Element of A9 st z <> y holds
z is_not_associated_to y

proof

let z, y be Element of A9; :: thesis: ( z <> y implies z is_not_associated_to y )
assume A6: z <> y ; :: thesis: z is_not_associated_to y

now :: thesis: ( ( z = 1. R & y = 1. R & z is_not_associated_to y ) or ( z = 1. R & y <> 1. R & ( z is_associated_to y implies z is_not_associated_to y ) ) or ( z <> 1. R & y = 1. R & ( z is_associated_to y implies z is_not_associated_to y ) ) or ( z <> 1. R & y <> 1. R & z is_not_associated_to y ) )

per cases ( ( z = 1. R & y = 1. R ) or ( z = 1. R & y <> 1. R ) or ( z <> 1. R & y = 1. R ) or ( z <> 1. R & y <> 1. R ) ) ;

case ( z = 1. R & y = 1. R ) ; :: thesis: z is_not_associated_to y

hence z is_not_associated_to y by A6; :: thesis: verum

end;

case A7: ( z = 1. R & y <> 1. R ) ; :: thesis: ( z is_associated_to y implies z is_not_associated_to y )

assume z is_associated_to y ; :: thesis: z is_not_associated_to y
not y in {(1. R)} by A7, TARSKI:def 1;
then y in { zz where zz is Element of A : zz <> x } by XBOOLE_0:def 3;
then ex zz being Element of A st
( y = zz & zz <> x ) ;
hence z is_not_associated_to y by A1, A7, Def7, Th4; :: thesis: verum

end;

case A8: ( z <> 1. R & y = 1. R ) ; :: thesis: ( z is_associated_to y implies z is_not_associated_to y )

assume z is_associated_to y ; :: thesis: z is_not_associated_to y
not z in {(1. R)} by A8, TARSKI:def 1;
then z in { zz where zz is Element of A : zz <> x } by XBOOLE_0:def 3;
then ex zz being Element of A st
( z = zz & zz <> x ) ;
hence z is_not_associated_to y by A1, A8, Def7, Th4; :: thesis: verum

end;

case ( z <> 1. R & y <> 1. R ) ; :: thesis: z is_not_associated_to y

then ( z in A & y in A ) by A3;
hence z is_not_associated_to y by A6, Def7; :: thesis: verum

end;

end;

end;

hence z is_not_associated_to y ; :: thesis: verum

end;

for a being Element of R ex z being Element of A9 st z is_associated_to a

proof

let a be Element of R; :: thesis: ex z being Element of A9 st z is_associated_to a

now :: thesis: ( ( a is_associated_to 1. R & ex z being Element of A9 st z is_associated_to a ) or ( a is_not_associated_to 1. R & ex z being Element of A9 st z is_associated_to a ) )

per cases ( a is_associated_to 1. R or a is_not_associated_to 1. R ) ;

case a is_associated_to 1. R ; :: thesis: ex z being Element of A9 st z is_associated_to a

hence ex z being Element of A9 st z is_associated_to a by A2; :: thesis: verum

end;

case A9: a is_not_associated_to 1. R ; :: thesis: ex z being Element of A9 st z is_associated_to a

consider z being Element of A such that
A10: z is_associated_to a by Def7;
z <> x by A1, A9, A10, Th4;
then z in { zz where zz is Element of A : zz <> x } ;
then z in A9 by XBOOLE_0:def 3;
hence ex z being Element of A9 st z is_associated_to a by A10; :: thesis: verum

end;

end;

end;

hence ex z being Element of A9 st z is_associated_to a ; :: thesis: verum

end;

then A9 is Am of R by A5, Def7;
hence ex b₁ being non empty Subset of R st
( b₁ is Am of R & 1. R in b₁ ) by A2; :: thesis: verum

end;

hence ex b₁ being non empty Subset of R st
( b₁ is Am of R & 1. R in b₁ ) ; :: thesis: verum