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