let X be set ; :: thesis: for A, B being Subset of X st A misses B holds
(A,B) followed_by {} is disjoint_valued
let A, B be Subset of X; :: thesis: ( A misses B implies (A,B) followed_by {} is disjoint_valued )
reconsider A1 = (A,B) followed_by ({} X) as SetSequence of X ;
assume A1: A misses B ; :: thesis: (A,B) followed_by {} is disjoint_valued
A1 is disjoint_valued

proof

A2: A1 . 1 = B by FUNCT_7:123;
let m, n be Nat; :: according to PROB_3:def 4 :: thesis: ( m = n or A1 . m misses A1 . n )
assume A3: m <> n ; :: thesis: A1 . m misses A1 . n
A4: A1 . 0 = A by FUNCT_7:122;

per cases ( m = 0 or ( m <> 0 & m = 1 ) or ( m <> 0 & m <> 1 ) ) ;

suppose A5: m = 0 ; :: thesis: A1 . m misses A1 . n

then n >= 1 by A3, NAT_1:14;
then A6: n + 1 > 1 by NAT_1:13;

per cases ( n > 1 or n = 1 ) by A6, NAT_1:22;

suppose n > 1 ; :: thesis: A1 . m misses A1 . n

then A1 . n = {} by FUNCT_7:124;
hence A1 . m misses A1 . n ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: A1 . m misses A1 . n

hence A1 . m misses A1 . n by A1, A4, A5, FUNCT_7:123; :: thesis: verum

end;

end;

end;

suppose A7: ( m <> 0 & m = 1 ) ; :: thesis: A1 . m misses A1 . n

( n >= 1 or n <= 1 ) ;
then A8: ( n + 1 > 1 or n < 1 + 1 ) by NAT_1:13;

per cases ( n > 1 or n = 0 ) by A3, A7, A8, NAT_1:14, NAT_1:22;

suppose n > 1 ; :: thesis: A1 . m misses A1 . n

then A1 . n = {} by FUNCT_7:124;
hence A1 . m misses A1 . n ; :: thesis: verum

end;

suppose n = 0 ; :: thesis: A1 . m misses A1 . n

hence A1 . m misses A1 . n by A1, A4, A2, A7; :: thesis: verum

end;

end;

end;

suppose A9: ( m <> 0 & m <> 1 ) ; :: thesis: A1 . m misses A1 . n

then m >= 1 by NAT_1:14;
then m + 1 > 1 by NAT_1:13;
then A1 . m = {} by A9, FUNCT_7:124, NAT_1:22;
hence A1 . m misses A1 . n ; :: thesis: verum

end;

end;

end;

hence (A,B) followed_by {} is disjoint_valued ; :: thesis: verum