deffunc H1( Element of RoughSets X, Element of RoughSets X) -> Element of RoughSets X = ((@ \$1) _\/_ (@ \$2)) @ ;
consider j being BinOp of () such that
A1: for x, y being Element of RoughSets X holds j . (x,y) = H1(x,y) from deffunc H2( Element of RoughSets X, Element of RoughSets X) -> Element of RoughSets X = ((@ \$1) _/\_ (@ \$2)) @ ;
consider m being BinOp of () such that
A2: for x, y being Element of RoughSets X holds m . (x,y) = H2(x,y) from take IT = LattStr(# (),j,m #); :: thesis: ( the carrier of IT = 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 IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 ) ) )

thus the carrier of IT = RoughSets X ; :: thesis: 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 IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 )

let A, B be Element of RoughSets X; :: thesis: for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 )

let A9, B9 be RoughSet of X; :: thesis: ( A = A9 & B = B9 implies ( the L_join of IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 ) )
assume A3: ( A = A9 & B = B9 ) ; :: thesis: ( the L_join of IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 )
thus the L_join of IT . (A,B) = H1(A,B) by A1
.= A9 _\/_ B9 by A3 ; :: thesis: the L_meet of IT . (A,B) = A9 _/\_ B9
thus the L_meet of IT . (A,B) = H2(A,B) by A2
.= A9 _/\_ B9 by A3 ; :: thesis: verum