let n be Nat; :: thesis: for no being Element of OrderedNAT st n = no holds

uparrow no = NAT \ (Segm n)

let no be Element of OrderedNAT; :: thesis: ( n = no implies uparrow no = NAT \ (Segm n) )

assume A1: n = no ; :: thesis: uparrow no = NAT \ (Segm n)

A2: uparrow no c= NAT \ (Segm n)

uparrow no = NAT \ (Segm n)

let no be Element of OrderedNAT; :: thesis: ( n = no implies uparrow no = NAT \ (Segm n) )

assume A1: n = no ; :: thesis: uparrow no = NAT \ (Segm n)

A2: uparrow no c= NAT \ (Segm n)

proof

NAT \ (Segm n) c= uparrow no
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow no or x in NAT \ (Segm n) )

assume A3: x in uparrow no ; :: thesis: x in NAT \ (Segm n)

then x in { x where x is Element of NAT : ex p0 being Element of NAT st

( no = p0 & p0 <= x ) } by CARDFIL2:50;

then ex y being Element of NAT st

( y = x & ex p0 being Element of NAT st

( no = p0 & p0 <= y ) ) ;

then reconsider y = x as Element of NAT ;

not y in Segm n by A1, A3, Th12, NAT_1:44;

hence x in NAT \ (Segm n) by XBOOLE_0:def 5; :: thesis: verum

end;assume A3: x in uparrow no ; :: thesis: x in NAT \ (Segm n)

then x in { x where x is Element of NAT : ex p0 being Element of NAT st

( no = p0 & p0 <= x ) } by CARDFIL2:50;

then ex y being Element of NAT st

( y = x & ex p0 being Element of NAT st

( no = p0 & p0 <= y ) ) ;

then reconsider y = x as Element of NAT ;

not y in Segm n by A1, A3, Th12, NAT_1:44;

hence x in NAT \ (Segm n) by XBOOLE_0:def 5; :: thesis: verum

proof

hence
uparrow no = NAT \ (Segm n)
by A2; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT \ (Segm n) or x in uparrow no )

assume A4: x in NAT \ (Segm n) ; :: thesis: x in uparrow no

then A5: ( x in NAT & not x in Segm n ) by XBOOLE_0:def 5;

reconsider y = x as Element of NAT by A4;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

( n1 <= y & n1 = no ) by A1, A5, NAT_1:44;

then y in { x where x is Element of NAT : ex p0 being Element of NAT st

( no = p0 & p0 <= x ) } ;

hence x in uparrow no by CARDFIL2:50; :: thesis: verum

end;assume A4: x in NAT \ (Segm n) ; :: thesis: x in uparrow no

then A5: ( x in NAT & not x in Segm n ) by XBOOLE_0:def 5;

reconsider y = x as Element of NAT by A4;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

( n1 <= y & n1 = no ) by A1, A5, NAT_1:44;

then y in { x where x is Element of NAT : ex p0 being Element of NAT st

( no = p0 & p0 <= x ) } ;

hence x in uparrow no by CARDFIL2:50; :: thesis: verum