let T be 1-sorted ; :: thesis: for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P
let P, Q be Subset of T; :: thesis: ( [#] T = P \/ Q & P misses Q implies Q = ([#] T) \ P )
assume that
A1: [#] T = P \/ Q and
A2: P misses Q ; :: thesis: Q = ([#] T) \ P
([#] T) \ P = Q \ P by A1, XBOOLE_1:40
.= Q by A2, XBOOLE_1:83 ;
hence Q = ([#] T) \ P ; :: thesis: verum