let A1, A2 be strict LattStr ; :: thesis: ( the carrier of A1 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A1 . (A,B) = A9 _\/_ B9 & the L_meet of A1 . (A,B) = A9 _/\_ B9 ) ) & the carrier of A2 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A2 . (A,B) = A9 _\/_ B9 & the L_meet of A2 . (A,B) = A9 _/\_ B9 ) ) implies A1 = A2 )

assume that

A4: ( the carrier of A1 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A1 . (A,B) = A9 _\/_ B9 & the L_meet of A1 . (A,B) = A9 _/\_ B9 ) ) ) and

A5: ( the carrier of A2 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A2 . (A,B) = A9 _\/_ B9 & the L_meet of A2 . (A,B) = A9 _/\_ B9 ) ) ) ; :: thesis: A1 = A2

reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (RoughSets X) by A4, A5;

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A1 . (A,B) = A9 _\/_ B9 & the L_meet of A1 . (A,B) = A9 _/\_ B9 ) ) & the carrier of A2 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A2 . (A,B) = A9 _\/_ B9 & the L_meet of A2 . (A,B) = A9 _/\_ B9 ) ) implies A1 = A2 )

assume that

A4: ( the carrier of A1 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A1 . (A,B) = A9 _\/_ B9 & the L_meet of A1 . (A,B) = A9 _/\_ B9 ) ) ) and

A5: ( the carrier of A2 = RoughSets X & ( for A, B being Element of RoughSets X

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of A2 . (A,B) = A9 _\/_ B9 & the L_meet of A2 . (A,B) = A9 _/\_ B9 ) ) ) ; :: thesis: A1 = A2

reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (RoughSets X) by A4, A5;

now :: thesis: for x, y being Element of RoughSets X holds a1 . (x,y) = a2 . (x,y)

then A6:
a1 = a2
by BINOP_1:2;let x, y be Element of RoughSets X; :: thesis: a1 . (x,y) = a2 . (x,y)

thus a1 . (x,y) = (@ x) _\/_ (@ y) by A4

.= a2 . (x,y) by A5 ; :: thesis: verum

end;thus a1 . (x,y) = (@ x) _\/_ (@ y) by A4

.= a2 . (x,y) by A5 ; :: thesis: verum

now :: thesis: for x, y being Element of RoughSets X holds a3 . (x,y) = a4 . (x,y)

hence
A1 = A2
by A4, A5, A6, BINOP_1:2; :: thesis: verumlet x, y be Element of RoughSets X; :: thesis: a3 . (x,y) = a4 . (x,y)

thus a3 . (x,y) = (@ x) _/\_ (@ y) by A4

.= a4 . (x,y) by A5 ; :: thesis: verum

end;thus a3 . (x,y) = (@ x) _/\_ (@ y) by A4

.= a4 . (x,y) by A5 ; :: thesis: verum