let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for S1, S2 being Subset of L holds - (S1 /\ S2) = (- S1) /\ (- S2)
let S1, S2 be Subset of L; :: thesis: - (S1 /\ S2) = (- S1) /\ (- S2)

A: now :: thesis: for o being object st o in - (S1 /\ S2) holds
o in (- S1) /\ (- S2)

let o be object ; :: thesis: ( o in - (S1 /\ S2) implies o in (- S1) /\ (- S2) )
assume o in - (S1 /\ S2) ; :: thesis: o in (- S1) /\ (- S2)
then consider s being Element of L such that
A: ( - s = o & s in S1 /\ S2 ) ;
( s in S1 & s in S2 ) by A, XBOOLE_0:def 4;
then ( - s in - S1 & - s in - S2 ) ;
hence o in (- S1) /\ (- S2) by A, XBOOLE_0:def 4; :: thesis: verum

end;

now :: thesis: for o being object st o in (- S1) /\ (- S2) holds
o in - (S1 /\ S2)

let o be object ; :: thesis: ( o in (- S1) /\ (- S2) implies o in - (S1 /\ S2) )
assume o in (- S1) /\ (- S2) ; :: thesis: o in - (S1 /\ S2)
then A: ( o in - S1 & o in - S2 ) by XBOOLE_0:def 4;
then consider s1 being Element of L such that
B: ( - s1 = o & s1 in S1 ) ;
consider s2 being Element of L such that
C: ( - s2 = o & s2 in S2 ) by A;
s1 = - (- s2) by B, C
.= s2 ;
then s1 in S1 /\ S2 by B, C, XBOOLE_0:def 4;
hence o in - (S1 /\ S2) by B; :: thesis: verum

end;

hence - (S1 /\ S2) = (- S1) /\ (- S2) by A, TARSKI:2; :: thesis: verum