let v, x be object ; :: thesis: for V, A being set
for p being SCPartialNominativePredicate of V,A holds
( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
let V, A be set ; :: thesis: for p being SCPartialNominativePredicate of V,A holds
( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
let p be SCPartialNominativePredicate of V,A; :: thesis: ( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
assume A1: x in dom (SC_exists (p,v)) ; :: thesis: ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
dom (SC_exists (p,v)) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } by Def1;
then ex d2 being TypeSCNominativeData of V,A st
( x = d2 & ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d2,d1,v) in dom p & p . (local_overlapping (V,A,d2,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d2,d1,v) in dom p & p . (local_overlapping (V,A,d2,d1,v)) = FALSE ) ) ) by A1;
hence ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) ; :: thesis: verum