now

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 A' = { z where z is Element of A : z <> x } \/ {(1. R)};
A2: 1. R in { z where z is Element of A : z <> x } \/ {(1. R)}

proof

1. R in {(1. R)} by TARSKI:def 1;
hence 1. R in { z where z is Element of A : z <> x } \/ {(1. R)} by XBOOLE_0:def 3; :: thesis: verum

end;

reconsider A' = { z where z is Element of A : z <> x } \/ {(1. R)} as non empty set ;
A3: for x being Element of A' holds
( x = 1. R or x in A )

proof

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

now

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

case 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;

case 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;

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

end;

A' is non empty Subset of R

proof

now

let x be set ; :: thesis: ( x in A' implies x in the carrier of R )

now

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

proof

now

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 A' implies x in the carrier of R ) ; :: thesis: verum

end;

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

end;

hence A' is non empty Subset of R by TARSKI:def 3; :: thesis: verum

end;

then reconsider A' = A' as non empty Subset of R ;
A5: for a being Element of R ex z being Element of A' st z is_associated_to a

proof

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

now

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 A' st z is_associated_to a

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

end;

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

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

end;

end;

end;

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

end;

for z, y being Element of A' st z <> y holds
z is_not_associated_to y

proof

let z, y be Element of A'; :: thesis: ( z <> y implies z is_not_associated_to y )
assume A8: z <> y ; :: thesis: z is_not_associated_to y

now

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 A8; :: thesis: verum

end;

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

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

end;

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

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

end;

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

then A14: z in A by A3;
y in A by A3, A13;
hence z is_not_associated_to y by A8, A14, Def7; :: thesis: verum

end;

end;

end;

hence z is_not_associated_to y ; :: thesis: verum

end;

then A' 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