reconsider X = D \/ (rng R) as non empty set ;
take X ; :: thesis: for b₁ being Formula st D,R |- b₁ holds
b₁ in X
thus for b₁ being Formula st D,R |- b₁ holds
b₁ in X by Lm54; :: thesis: verum