let R be non empty RelStr ; :: thesis: for A, B being Subset of R holds (LAp R) . (A /\ B) = ((LAp R) . A) /\ ((LAp R) . B)
let X, Y be Subset of R; :: thesis: (LAp R) . (X /\ Y) = ((LAp R) . X) /\ ((LAp R) . Y)
set L = LAp R;
(LAp R) . (X /\ Y) = LAp (X /\ Y) by ROUGHS_2:def 10
.= (LAp X) /\ (LAp Y) by ROUGHS_2:12
.= ((LAp R) . X) /\ (LAp Y) by ROUGHS_2:def 10
.= ((LAp R) . X) /\ ((LAp R) . Y) by ROUGHS_2:def 10 ;
hence (LAp R) . (X /\ Y) = ((LAp R) . X) /\ ((LAp R) . Y) ; :: thesis: verum