let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being bag of the carrier of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
a = b | { x where x is Element of R : x is_maximal_in support b }
let a, b be bag of the carrier of R; :: thesis: for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
a = b | { x where x is Element of R : x is_maximal_in support b }
let p be partition of b -' a; :: thesis: for q being partition of b st q is ordered & q = <*a*> ^ p holds
a = b | { x where x is Element of R : x is_maximal_in support b }
let q be partition of b; :: thesis: ( q is ordered & q = <*a*> ^ p implies a = b | { x where x is Element of R : x is_maximal_in support b } )
assume Z0: q is ordered ; :: thesis: ( not q = <*a*> ^ p or a = b | { x where x is Element of R : x is_maximal_in support b } )
assume Z1: q = <*a*> ^ p ; :: thesis: a = b | { x where x is Element of R : x is_maximal_in support b }
let y be Element of R; :: according to PBOOLE:def 21 :: thesis: a . y = (b | { x where x is Element of R : x is_maximal_in support b } ) . y
set J = { x where x is Element of R : x is_maximal_in support b } ;
per cases ( y in { x where x is Element of R : x is_maximal_in support b } or not y in { x where x is Element of R : x is_maximal_in support b } ) ;
suppose A0: y in { x where x is Element of R : x is_maximal_in support b } ; :: thesis: a . y = (b | { x where x is Element of R : x is_maximal_in support b } ) . y
then consider x being Element of R such that
A1: ( y = x & x is_maximal_in support b ) ;
a . y > 0 by Z0, Z1, A1, Th34;
hence a . y = b . y by Z0, Z1, Th31
.= (b | { x where x is Element of R : x is_maximal_in support b } ) . y by A0, BAR ;
:: thesis: verum
end;
suppose A2: not y in { x where x is Element of R : x is_maximal_in support b } ; :: thesis: a . y = (b | { x where x is Element of R : x is_maximal_in support b } ) . y
then not y is_maximal_in support b ;
then a . y <= 0 by Z0, Z1, Th34;
hence a . y = 0
.= (b | { x where x is Element of R : x is_maximal_in support b } ) . y by A2, BAR ;
:: thesis: verum
end;
end;