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

now :: thesis: ( ( p in IPC-Taut & p 'or' q in IPC-Taut ) or ( q in IPC-Taut & p 'or' q in IPC-Taut ) )

per cases ( p in IPC-Taut or q in IPC-Taut ) by A1;

case A2: p in IPC-Taut ; :: thesis: p 'or' q in IPC-Taut

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

end;

case A3: q in IPC-Taut ; :: thesis: p 'or' q in IPC-Taut

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

end;

end;

end;

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