now

let R be non empty associative well-unital multLoopStr ; :: thesis: ex s being non empty Subset of R st
( ( for a being Element of R ex z being Element of s st z is_associated_to a ) & ( for x, y being Element of s st x <> y holds
x is_not_associated_to y ) )
reconsider M = Classes R as non empty set ;
A1: for X being set st X in M holds
X <> {}

proof

let X be set ; :: thesis: ( X in M implies X <> {} )
assume X in M ; :: thesis: X <> {}
then consider A being Element of R such that
A2: X = Class A by Def6;
thus X <> {} by A2; :: thesis: verum

end;

for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y

proof

let X, Y be set ; :: thesis: ( X in M & Y in M & X <> Y implies X misses Y )
assume A3: ( X in M & Y in M & X <> Y ) ; :: thesis: X misses Y
assume A4: X meets Y ; :: thesis: contradiction
consider A being Element of R such that
A5: X = Class A by A3, Def6;
consider B being Element of R such that
A6: Y = Class B by A3, Def6;
thus contradiction by A3, A4, A5, A6, Th20; :: thesis: verum

end;

then consider AmpS' being set such that
A7: for X being set st X in M holds
ex x being set st AmpS' /\ X = {x} by A1, WELLORD2:27;
not AmpS' is empty

proof

Class (1. R) in M by Def6;
then consider x being set such that
A8: AmpS' /\ (Class (1. R)) = {x} by A7;
thus not AmpS' is empty by A8; :: thesis: verum

end;

then reconsider AmpS' = AmpS' as non empty set ;
set AmpS = { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } ;
A9: for X being Element of M ex z being Element of { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } st { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X = {z}

proof

let X be Element of M; :: thesis: ex z being Element of { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } st { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X = {z}
consider x being set such that
A10: AmpS' /\ X = {x} by A7;
X in Classes R ;
then A11: X is non empty Subset of R by Th21;
A12: x in {x} by TARSKI:def 1;
then A13: x in AmpS' by A10, XBOOLE_0:def 4;
A14: x in X by A10, A12, XBOOLE_0:def 4;
A15: x in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } by A10, A11, A13;
{ x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X = {x}

proof

now

let y be set ; :: thesis: ( y in {x} iff y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X )

A16: now

assume y in {x} ; :: thesis: ( y in {x} implies y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X )
then y = x by TARSKI:def 1;
hence ( y in {x} implies y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X ) by A14, A15, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume A17: y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X ; :: thesis: ( y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X implies y in {x} )
then A18: y in X by XBOOLE_0:def 4;
y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } by A17, XBOOLE_0:def 4;
then consider zz being Element of AmpS' such that
A19: ( y = zz & ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {zz} ) ) ;
thus ( y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X implies y in {x} ) by A10, A18, A19, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( y in {x} iff y in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X ) by A16; :: thesis: verum

end;

hence { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X = {x} by TARSKI:2; :: thesis: verum

end;

hence ex z being Element of { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } st { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } /\ X = {z} by A15; :: thesis: verum

end;

{ x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } is non empty Subset of R

proof

not { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } is empty

proof

A20: Class (1. R) in M by Def6;
then consider x being set such that
A21: AmpS' /\ (Class (1. R)) = {x} by A7;
x in {x} by TARSKI:def 1;
then x in AmpS' by A21, XBOOLE_0:def 4;
then x in { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } by A20, A21;
hence not { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } is empty ; :: thesis: verum

end;

then reconsider AmpS = { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } as non empty set ;

now

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

now

assume A in AmpS ; :: thesis: ( A in AmpS implies A in the carrier of R )
then consider x being Element of AmpS' such that
A22: ( A = x & ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) ) ;
consider X being non empty Subset of R;
x in {x} by TARSKI:def 1;
hence ( A in AmpS implies A in the carrier of R ) by A22; :: thesis: verum

end;

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

end;

hence { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } is non empty Subset of R by TARSKI:def 3; :: thesis: verum

end;

then reconsider AmpS = { x where x is Element of AmpS' : ex X being non empty Subset of R st
( X in M & AmpS' /\ X = {x} ) } as non empty Subset of R ;
A23: for a being Element of R ex z being Element of AmpS st z is_associated_to a

proof

let a be Element of R; :: thesis: ex z being Element of AmpS st z is_associated_to a
reconsider N = Class a as Element of M by Def6;
consider z being Element of AmpS such that
A24: AmpS /\ N = {z} by A9;
z in {z} by TARSKI:def 1;
then z in Class a by A24, XBOOLE_0:def 4;
then z is_associated_to a by Def5;
hence ex z being Element of AmpS st z is_associated_to a ; :: thesis: verum

end;

for x, y being Element of AmpS st x <> y holds
x is_not_associated_to y

proof

let x, y be Element of AmpS; :: thesis: ( x <> y implies x is_not_associated_to y )
assume A25: x <> y ; :: thesis: x is_not_associated_to y
assume A26: x is_associated_to y ; :: thesis: contradiction
x is_associated_to x ;
then A27: x in Class x by Def5;
A28: y in Class x by A26, Def5;
A29: x in AmpS /\ (Class x) by A27, XBOOLE_0:def 4;
A30: y in AmpS /\ (Class x) by A28, XBOOLE_0:def 4;
Class x in M by Def6;
then consider z being Element of AmpS such that
A31: AmpS /\ (Class x) = {z} by A9;
y = z by A30, A31, TARSKI:def 1;
hence contradiction by A25, A29, A31, TARSKI:def 1; :: thesis: verum

end;

hence ex s being non empty Subset of R st
( ( for a being Element of R ex z being Element of s st z is_associated_to a ) & ( for x, y being Element of s st x <> y holds
x is_not_associated_to y ) ) by A23; :: thesis: verum

end;

hence ex b₁ being non empty Subset of R st
( ( for a being Element of R ex z being Element of b₁ st z is_associated_to a ) & ( for x, y being Element of b₁ st x <> y holds
x is_not_associated_to y ) ) ; :: thesis: verum