let R be non empty associative multLoopStr ; :: thesis: for a, b being Element of R st Class a meets Class b holds
Class a = Class b
let a, b be Element of R; :: thesis: ( Class a meets Class b implies Class a = Class b )
assume (Class a) /\ (Class b) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: Class a = Class b
then Class a meets Class b ;
then consider Z being object such that
A1: Z in Class a and
A2: Z in Class b by XBOOLE_0:3;
reconsider Z = Z as Element of R by A1;
A3: Z is_associated_to b by A2, Def5;
A4: Z is_associated_to a by A1, Def5;
A5: for c being Element of R st c in Class b holds
c in Class a
proof
let c be Element of R; :: thesis: ( c in Class b implies c in Class a )
assume c in Class b ; :: thesis: c in Class a
then c is_associated_to b by Def5;
then Z is_associated_to c by A3, Th4;
then a is_associated_to c by A4, Th4;
hence c in Class a by Def5; :: thesis: verum
end;
for c being Element of R st c in Class a holds
c in Class b
proof
let c be Element of R; :: thesis: ( c in Class a implies c in Class b )
assume c in Class a ; :: thesis: c in Class b
then c is_associated_to a by Def5;
then Z is_associated_to c by A4, Th4;
then b is_associated_to c by A3, Th4;
hence c in Class b by Def5; :: thesis: verum
end;
hence Class a = Class b by A5, SUBSET_1:3; :: thesis: verum