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)
proof
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;
NAT \ (Segm n) c= uparrow no
proof
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;
hence uparrow no = NAT \ (Segm n) by A2; :: thesis: verum