let X be set ; 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; ([: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; verum