let p, q be Element of MC-wff ; :: thesis:
assume A1: ( p in IPC-Taut or q in IPC-Taut ) ; :: thesis:

per cases by A1;

case A2: p in IPC-Taut ; :: thesis:

p => (p 'or' q) in IPC-Taut by Def14;
hence p 'or' q in IPC-Taut by A2, Def14; :: thesis:

end;

case A3: q in IPC-Taut ; :: thesis:

q => (p 'or' q) in IPC-Taut by Def14;
hence p 'or' q in IPC-Taut by A3, Def14; :: thesis:

end;

end;

end;

hence p 'or' q in IPC-Taut ; :: thesis: