let k be Element of NAT ; :: thesis: for d being non zero Element of NAT
for G being Grating of d st k + 1 <= d holds
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )
let d be non zero Element of NAT ; :: thesis: for G being Grating of d st k + 1 <= d holds
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )
let G be Grating of d; :: thesis: ( k + 1 <= d implies for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B ) )
assume A1: k + 1 <= d ; :: thesis: for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )
let A be Cell of k,G; :: thesis: for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )
let B be Cell of (k + 1),G; :: thesis: ( A in del {B} iff A c= B )
set X = (star A) /\ {B};
( not card ((star A) /\ {B}) is even iff B in star A )

proof

per cases ( B in star A or not B in star A ) ;

suppose A2: B in star A ; :: thesis: ( not card ((star A) /\ {B}) is even iff B in star A )

now

let B' be set ; :: thesis: ( B' in (star A) /\ {B} iff B' = B )
( B' in {B} iff B' = B ) by TARSKI:def 1;
hence ( B' in (star A) /\ {B} iff B' = B ) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

then (star A) /\ {B} = {B} by TARSKI:def 1;
then card ((star A) /\ {B}) = (2 * 0 ) + 1 by CARD_1:50;
hence ( not card ((star A) /\ {B}) is even iff B in star A ) by A2; :: thesis: verum

end;

suppose A3: not B in star A ; :: thesis: ( not card ((star A) /\ {B}) is even iff B in star A )

now

let B' be set ; :: thesis: not B' in (star A) /\ {B}
( B' = B or not B' in {B} ) by TARSKI:def 1;
hence not B' in (star A) /\ {B} by A3, XBOOLE_0:def 4; :: thesis: verum

end;

then card ((star A) /\ {B}) = 2 * 0 by CARD_1:47, XBOOLE_0:def 1;
hence ( not card ((star A) /\ {B}) is even iff B in star A ) by A3; :: thesis: verum

end;

end;

end;

hence ( A in del {B} iff A c= B ) by A1, Th51, Th52; :: thesis: verum