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 )
proof
per cases ( B in star A or not B in star A ) ;
suppose A2: B in star A ; :: thesis: ( card ((star A) /\ {B}) is odd iff B in star A )
now :: thesis: for B9 being object holds
( 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;
then (star A) /\ {B} = {B} by TARSKI:def 1;
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;
suppose A3: not B in star A ; :: thesis: ( card ((star A) /\ {B}) is odd iff B in star A )
now :: thesis: for B9 being object holds not B9 in (star A) /\ {B}
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;
then card ((star A) /\ {B}) = 2 * 0 by CARD_1:27, XBOOLE_0:def 1;
hence ( card ((star A) /\ {B}) is odd iff B in star A ) by A3; :: thesis: verum
end;
end;
end;
hence ( A in del {B} iff A c= B ) by A1, Th47, Th48; :: thesis: verum