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 or s in S2 ) by A, XBOOLE_0:def 3;
then ( - s in - S1 or - s in - S2 ) ;
hence o in (- S1) \/ (- S2) by A, XBOOLE_0:def 3; :: 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 b1 in - (S1 \/ S2) )
assume A: o in (- S1) \/ (- S2) ; :: thesis: b1 in - (S1 \/ S2)
per cases ( o in - S1 or o in - S2 ) by A, XBOOLE_0:def 3;
suppose o in - S1 ; :: thesis: b1 in - (S1 \/ S2)
then consider s1 being Element of L such that
B: ( - s1 = o & s1 in S1 ) ;
s1 in S1 \/ S2 by B, XBOOLE_0:def 3;
hence o in - (S1 \/ S2) by B; :: thesis: verum
end;
suppose o in - S2 ; :: thesis: b1 in - (S1 \/ S2)
then consider s1 being Element of L such that
B: ( - s1 = o & s1 in S2 ) ;
s1 in S1 \/ S2 by B, XBOOLE_0:def 3;
hence o in - (S1 \/ S2) by B; :: thesis: verum
end;
end;
end;
hence - (S1 \/ S2) = (- S1) \/ (- S2) by A, TARSKI:2; :: thesis: verum