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 A', B' being RoughSet of X st A = A' & B = B' holds
( the L_join of IT . A,B = A' _\/_ B' & the L_meet of IT . A,B = A' _/\_ B' ) ) )
thus the carrier of IT = RoughSets X ; :: thesis: for A, B being Element of RoughSets X
for A', B' being RoughSet of X st A = A' & B = B' holds
( the L_join of IT . A,B = A' _\/_ B' & the L_meet of IT . A,B = A' _/\_ B' )
let A, B be Element of RoughSets X; :: thesis: for A', B' being RoughSet of X st A = A' & B = B' holds
( the L_join of IT . A,B = A' _\/_ B' & the L_meet of IT . A,B = A' _/\_ B' )
let A', B' be RoughSet of X; :: thesis: ( A = A' & B = B' implies ( the L_join of IT . A,B = A' _\/_ B' & the L_meet of IT . A,B = A' _/\_ B' ) )
assume B2: ( A = A' & B = B' ) ; :: thesis: ( the L_join of IT . A,B = A' _\/_ B' & the L_meet of IT . A,B = A' _/\_ B' )
thus the L_join of IT . A,B = H₁(A,B) by A1
.= A' _\/_ B' by B2 ; :: thesis: the L_meet of IT . A,B = A' _/\_ B'
thus the L_meet of IT . A,B = H₂(A,B) by A2
.= A' _/\_ B' by B2 ; :: thesis: verum