let p, q, r, s be boolean object ; :: thesis: ( p <=> q = TRUE & r <=> s = TRUE implies (p 'or' r) <=> (q 'or' s) = TRUE )
( p = FALSE or p = TRUE ) by Def3;
hence ( p <=> q = TRUE & r <=> s = TRUE implies (p 'or' r) <=> (q 'or' s) = TRUE ) ; :: thesis: verum