let x, y, c be non pair set ; for s being State of (BorrowCirc (x,y,c))
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2
reconsider a = c as Vertex of (BorrowStr (x,y,c)) by Th6;
let s be State of (BorrowCirc (x,y,c)); for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2
s . a is Element of BOOLEAN
;
hence
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2
by Lm1; verum