let R be non empty multLoopStr ; :: thesis: for I, J, K being Subset of R holds (J /\ K) % I = (J % I) /\ (K % I)
let I, J, K be Subset of R; :: thesis: (J /\ K) % I = (J % I) /\ (K % I)

A1: now :: thesis: for u being object st u in (J /\ K) % I holds
u in (J % I) /\ (K % I)

let u be object ; :: thesis: ( u in (J /\ K) % I implies u in (J % I) /\ (K % I) )
assume u in (J /\ K) % I ; :: thesis: u in (J % I) /\ (K % I)
then consider a being Element of R such that
A2: u = a and
A3: a * I c= J /\ K ;

now :: thesis: for v being object st v in a * I holds
v in K

let v be object ; :: thesis: ( v in a * I implies v in K )
assume v in a * I ; :: thesis: v in K
then v in J /\ K by A3;
then ex x being Element of R st
( v = x & x in J & x in K ) ;
hence v in K ; :: thesis: verum

end;

then a * I c= K ;
then A4: u in K % I by A2;

now :: thesis: for v being object st v in a * I holds
v in J

let v be object ; :: thesis: ( v in a * I implies v in J )
assume v in a * I ; :: thesis: v in J
then v in J /\ K by A3;
then ex x being Element of R st
( v = x & x in J & x in K ) ;
hence v in J ; :: thesis: verum

end;

then a * I c= J ;
then u in J % I by A2;
hence u in (J % I) /\ (K % I) by A4; :: thesis: verum

end;

now :: thesis: for u being object st u in (J % I) /\ (K % I) holds
u in (J /\ K) % I

let u be object ; :: thesis: ( u in (J % I) /\ (K % I) implies u in (J /\ K) % I )
assume u in (J % I) /\ (K % I) ; :: thesis: u in (J /\ K) % I
then A5: ex x being Element of R st
( x = u & x in J % I & x in K % I ) ;
then consider a being Element of R such that
A6: u = a and
A7: a * I c= J ;
ex b being Element of R st
( u = b & b * I c= K ) by A5;
then for v being object st v in a * I holds
v in J /\ K by A6, A7;
then a * I c= J /\ K ;
hence u in (J /\ K) % I by A6; :: thesis: verum

end;

hence (J /\ K) % I = (J % I) /\ (K % I) by A1, TARSKI:2; :: thesis: verum