deffunc H_{1}( Element of RoughSets X, Element of RoughSets X) -> Element of RoughSets X = ((@ $1) _\/_ (@ $2)) @ ;

consider j being BinOp of (RoughSets X) such that

A1: for x, y being Element of RoughSets X holds j . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

deffunc H_{2}( Element of RoughSets X, Element of RoughSets X) -> Element of RoughSets X = ((@ $1) _/\_ (@ $2)) @ ;

consider m being BinOp of (RoughSets X) such that

A2: for x, y being Element of RoughSets X holds m . (x,y) = H_{2}(x,y)
from BINOP_1:sch 4();

take IT = LattStr(# (RoughSets X),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) = H_{1}(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) = H_{2}(A,B)
by A2

.= A9 _/\_ B9 by A3 ; :: thesis: verum

consider j being BinOp of (RoughSets X) such that

A1: for x, y being Element of RoughSets X holds j . (x,y) = H

deffunc H

consider m being BinOp of (RoughSets X) such that

A2: for x, y being Element of RoughSets X holds m . (x,y) = H

take IT = LattStr(# (RoughSets X),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) = H

.= A9 _\/_ B9 by A3 ; :: thesis: the L_meet of IT . (A,B) = A9 _/\_ B9

thus the L_meet of IT . (A,B) = H

.= A9 _/\_ B9 by A3 ; :: thesis: verum