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