A1: now :: thesis: ( a = o & b = o & the addF of R . (x,x) <> x implies the addF of R . (x,x) is Element of carr (x,o) )
assume ( a = o & b = o & the addF of R . (x,x) <> x ) ; :: thesis: the addF of R . (x,x) is Element of carr (x,o)
then not the addF of R . (x,x) in {x} by TARSKI:def 1;
then the addF of R . (x,x) in ([#] R) \ {x} by XBOOLE_0:def 5;
hence the addF of R . (x,x) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum
end;
A2: now :: thesis: ( a <> o & b = o & the addF of R . (a,x) <> x implies the addF of R . (a,x) is Element of carr (x,o) )
assume A3: ( a <> o & b = o & the addF of R . (a,x) <> x ) ; :: thesis: the addF of R . (a,x) is Element of carr (x,o)
then not a in {o} by TARSKI:def 1;
then a in ([#] R) \ {x} by XBOOLE_0:def 3;
then reconsider a1 = a as Element of [#] R ;
not the addF of R . (a,x) in {x} by A3, TARSKI:def 1;
then the addF of R . (a1,x) in ([#] R) \ {x} by XBOOLE_0:def 5;
hence the addF of R . (a,x) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum
end;
A4: now :: thesis: ( a = o & b <> o & the addF of R . (x,b) <> x implies the addF of R . (x,b) is Element of carr (x,o) )
assume A5: ( a = o & b <> o & the addF of R . (x,b) <> x ) ; :: thesis: the addF of R . (x,b) is Element of carr (x,o)
then not b in {o} by TARSKI:def 1;
then b in ([#] R) \ {x} by XBOOLE_0:def 3;
then reconsider b1 = b as Element of [#] R ;
not the addF of R . (x,b) in {x} by A5, TARSKI:def 1;
then the addF of R . (x,b1) in ([#] R) \ {x} by XBOOLE_0:def 5;
hence the addF of R . (x,b) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum
end;
A6: now :: thesis: ( a <> o & b <> o & the addF of R . (a,b) <> x implies the addF of R . (a,b) is Element of carr (x,o) )
assume A7: ( a <> o & b <> o & the addF of R . (a,b) <> x ) ; :: thesis: the addF of R . (a,b) is Element of carr (x,o)
then not a in {o} by TARSKI:def 1;
then a in ([#] R) \ {x} by XBOOLE_0:def 3;
then reconsider a1 = a as Element of [#] R ;
not b in {o} by A7, TARSKI:def 1;
then b in ([#] R) \ {x} by XBOOLE_0:def 3;
then reconsider b1 = b as Element of [#] R ;
not the addF of R . (a,b) in {x} by A7, TARSKI:def 1;
then the addF of R . (a1,b1) in ([#] R) \ {x} by XBOOLE_0:def 5;
hence the addF of R . (a,b) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum
end;
o in {o} by TARSKI:def 1;
hence ( ( a = o & b = o & the addF of R . (x,x) <> x implies the addF of R . (x,x) is Element of carr (x,o) ) & ( a <> o & b = o & the addF of R . (a,x) <> x implies the addF of R . (a,x) is Element of carr (x,o) ) & ( a = o & b <> o & the addF of R . (x,b) <> x implies the addF of R . (x,b) is Element of carr (x,o) ) & ( a <> o & b <> o & the addF of R . (a,b) <> x implies the addF of R . (a,b) is Element of carr (x,o) ) & ( ( not a = o or not b = o or not the addF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the addF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the addF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the addF of R . (a,b) <> x ) implies o is Element of carr (x,o) ) ) by A1, A2, A4, A6, XBOOLE_0:def 3; :: thesis: verum