let k be Nat; :: thesis: for d being non zero 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 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};

( card ((star A) /\ {B}) is odd iff B in star A )

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 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};

( card ((star A) /\ {B}) is odd iff B in star A )

proof
end;

hence
( A in del {B} iff A c= B )
by A1, Th47, Th48; :: thesis: verumper cases
( B in star A or not B in star A )
;

end;

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

then card ((star A) /\ {B}) = (2 * 0) + 1 by CARD_1:30;

hence ( card ((star A) /\ {B}) is odd iff B in star A ) by A2; :: thesis: verum

end;

now :: thesis: for B9 being object holds

( B9 in (star A) /\ {B} iff B9 = B )

then
(star A) /\ {B} = {B}
by TARSKI:def 1;( B9 in (star A) /\ {B} iff B9 = B )

let B9 be object ; :: thesis: ( B9 in (star A) /\ {B} iff B9 = B )

( B9 in {B} iff B9 = B ) by TARSKI:def 1;

hence ( B9 in (star A) /\ {B} iff B9 = B ) by A2, XBOOLE_0:def 4; :: thesis: verum

end;( B9 in {B} iff B9 = B ) by TARSKI:def 1;

hence ( B9 in (star A) /\ {B} iff B9 = B ) by A2, XBOOLE_0:def 4; :: thesis: verum

then card ((star A) /\ {B}) = (2 * 0) + 1 by CARD_1:30;

hence ( card ((star A) /\ {B}) is odd iff B in star A ) by A2; :: thesis: verum

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

hence ( card ((star A) /\ {B}) is odd iff B in star A ) by A3; :: thesis: verum

end;

now :: thesis: for B9 being object holds not B9 in (star A) /\ {B}

then
card ((star A) /\ {B}) = 2 * 0
by CARD_1:27, XBOOLE_0:def 1;let B9 be object ; :: thesis: not B9 in (star A) /\ {B}

( B9 = B or not B9 in {B} ) by TARSKI:def 1;

hence not B9 in (star A) /\ {B} by A3, XBOOLE_0:def 4; :: thesis: verum

end;( B9 = B or not B9 in {B} ) by TARSKI:def 1;

hence not B9 in (star A) /\ {B} by A3, XBOOLE_0:def 4; :: thesis: verum

hence ( card ((star A) /\ {B}) is odd iff B in star A ) by A3; :: thesis: verum