let X be set ; :: thesis: for A being Subset of X holds ([:A,A:] \/ [:(X \ A),(X \ A):]) ~ = [:A,A:] \/ [:(X \ A),(X \ A):]
let A be Subset of X; :: thesis: ([:A,A:] \/ [:(X \ A),(X \ A):]) ~ = [:A,A:] \/ [:(X \ A),(X \ A):]
( [:A,A:] ~ = [:A,A:] & [:(X \ A),(X \ A):] ~ = [:(X \ A),(X \ A):] ) by SYSREL:5;
hence ([:A,A:] \/ [:(X \ A),(X \ A):]) ~ = [:A,A:] \/ [:(X \ A),(X \ A):] by RELAT_1:23; :: thesis: verum