now

let R be non empty associative well-unital multLoopStr ; :: thesis: ex s being non empty Subset of st
( ( for a being Element of 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 ex A being Element of st X = Class A by Def6;
hence X <> {} ; :: 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 that
A2: ( X in M & Y in M ) and
A3: X <> Y ; :: thesis: X misses Y
assume A4: X meets Y ; :: thesis: contradiction
( ex A being Element of st X = Class A & ex B being Element of st Y = Class B ) by A2, Def6;
hence contradiction by A3, A4, Th20; :: thesis: verum

end;

then consider AmpS' being set such that
A5: 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 ex x being set st AmpS' /\ (Class (1. R)) = {x} by A5;
hence not AmpS' is empty ; :: 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 st
( X in M & AmpS' /\ X = {x} ) } ;
A6: { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } is non empty Subset of

proof

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

proof

A7: Class (1. R) in M by Def6;
then consider x being set such that
A8: AmpS' /\ (Class (1. R)) = {x} by A5;
x in {x} by TARSKI:def 1;
then x in AmpS' by A8, XBOOLE_0:def 4;
then x in { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } by A7, A8;
hence not { x where x is Element of AmpS' : ex X being non empty Subset of 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 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

consider X being non empty Subset of ;
assume A in AmpS ; :: thesis: ( A in AmpS implies A in the carrier of R )
then consider x being Element of AmpS' such that
A9: ( A = x & ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) ) ;
x in {x} by TARSKI:def 1;
hence ( A in AmpS implies A in the carrier of R ) by A9; :: 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 st
( X in M & AmpS' /\ X = {x} ) } is non empty Subset of by TARSKI:def 3; :: thesis: verum

end;

A10: 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 st
( X in M & AmpS' /\ X = {x} ) } st { x where x is Element of AmpS' : ex X being non empty Subset of 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 st
( X in M & AmpS' /\ X = {x} ) } st { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } /\ X = {z}
consider x being set such that
A11: AmpS' /\ X = {x} by A5;
X in Classes R ;
then A12: X is non empty Subset of by Th21;
A13: x in {x} by TARSKI:def 1;
then x in AmpS' by A11, XBOOLE_0:def 4;
then A14: x in { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } by A11, A12;
A15: x in X by A11, A13, XBOOLE_0:def 4;

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 st
( X in M & AmpS' /\ X = {x} ) } /\ X )

A16: now

assume A17: y in { x where x is Element of AmpS' : ex X being non empty Subset of 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 st
( X in M & AmpS' /\ X = {x} ) } /\ X implies y in {x} )
then y in { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } by XBOOLE_0:def 4;
then A18: ex zz being Element of AmpS' st
( y = zz & ex X being non empty Subset of st
( X in M & AmpS' /\ X = {zz} ) ) ;
y in X by A17, XBOOLE_0:def 4;
hence ( y in { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } /\ X implies y in {x} ) by A11, A18, XBOOLE_0:def 4; :: thesis: verum

end;

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 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 st
( X in M & AmpS' /\ X = {x} ) } /\ X ) by A15, A14, 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 st
( X in M & AmpS' /\ X = {x} ) } /\ X ) by A16; :: thesis: verum

end;

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

end;

reconsider AmpS = { x where x is Element of AmpS' : ex X being non empty Subset of st
( X in M & AmpS' /\ X = {x} ) } as non empty Subset of by A6;
A19: 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 A20: x <> y ; :: thesis: x is_not_associated_to y
x is_associated_to x ;
then x in Class x by Def5;
then A21: x in AmpS /\ (Class x) by XBOOLE_0:def 4;
Class x in M by Def6;
then consider z being Element of AmpS such that
A22: AmpS /\ (Class x) = {z} by A10;
assume x is_associated_to y ; :: thesis: contradiction
then y in Class x by Def5;
then y in AmpS /\ (Class x) by XBOOLE_0:def 4;
then y = z by A22, TARSKI:def 1;
hence contradiction by A20, A21, A22, TARSKI:def 1; :: thesis: verum

end;

for a being Element of ex z being Element of AmpS st z is_associated_to a

proof

let a be Element of ; :: 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
A23: AmpS /\ N = {z} by A10;
z in {z} by TARSKI:def 1;
then z in Class a by A23, 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;

hence ex s being non empty Subset of st
( ( for a being Element of 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 A19; :: thesis: verum

end;

hence ex b₁ being non empty Subset of st
( ( for a being Element of 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