deffunc H₁( 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₁(x,y) from BINOP_1:sch 4();
deffunc H₂( 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₂(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₁(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₂(A,B) by A2
.= A9 _/\_ B9 by A3 ; :: thesis: verum